for a, b, c being real number st |.(a - b).| <= c holds
( b - c <= a & a <= b + c )

for r, s being real number st r < s holds
left_closed_halfline r misses right_closed_halfline s

for r, s being real number st r <= s holds
left_open_halfline r misses right_open_halfline s

for f, g, h being real-yielding Function st f c= g holds
h - f c= h - g

for f, g, h being real-yielding Function st f c= g holds
f - h c= g - h

for T1 being empty TopSpace
for T2 being TopSpace
for f being Function of T1,T2 holds f is continuous

for f, g being summable Real_Sequence st ( for n being Nat holds f . n <= g . n ) holds
Sum f <= Sum g

for f being Real_Sequence st f is absolutely_summable holds
abs (Sum f) <= Sum (abs f)

for f being Real_Sequence
for a, r being real positive number st r < 1 & ( for n being natural number holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( f is convergent & ( for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )

for f being Real_Sequence
for a, r being real positive number st r < 1 & ( for n being natural number holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) )

for X, Z being non empty set
for F being Functional_Sequence of X, REAL st Z common_on_dom F holds
for a, r being real positive number st r < 1 & ( for n being natural number holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_unif_conv_on Z & ( for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )

for X, Z being non empty set
for F being Functional_Sequence of X, REAL st Z common_on_dom F holds
for a, r being real positive number st r < 1 & ( for n being natural number holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
for z being Element of Z holds
( (lim F,Z) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim F,Z) . z <= ((F . 0) . z) + (a / (1 - r)) )

for X, Z being non empty set
for F being Functional_Sequence of X, REAL st Z common_on_dom F holds
for a, r being real positive number
for f being Function of Z, REAL st r < 1 & ( for n being natural number holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_point_conv_on Z & lim F,Z = f )

for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
for x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )

for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
rng (f1 union f2) c= (rng f1) \/ (rng f2)

for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )

for r being real number
for X being set
for f, g being real-yielding Function st f c= g & g,X is_absolutely_bounded_by r holds
f,X is_absolutely_bounded_by r

for r being real number
for X being set
for f, g being real-yielding Function st ( X c= dom f or dom g c= dom f ) & f | X = g | X & f,X is_absolutely_bounded_by r holds
g,X is_absolutely_bounded_by r

for r being real number
for T being non empty TopSpace
for A being closed Subset of T st r > 0 & T is being_T4 holds
for f being continuous Function of (T | A),R^1 st f,A is_absolutely_bounded_by r holds
ex g being continuous Function of T,R^1 st
( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 )

for T being non empty TopSpace st ( for A, B being non empty closed Subset of T st A misses B holds
ex f being continuous Function of T,R^1 st
( f .: A = {0} & f .: B = {1} ) ) holds
T is_T4

for T being non empty TopSpace
for f being Function of T,R^1
for x being Point of T holds
( f is_continuous_at x iff for e being real number st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
abs ((f . y) - (f . x)) < e ) ) )

for T being non empty TopSpace
for F being Functional_Sequence of the carrier of T, REAL st F is_unif_conv_on the carrier of T & ( for i being Nat holds F . i is continuous Function of T,R^1 ) holds
lim F,the carrier of T is continuous Function of T,R^1

for T being non empty TopSpace
for f being Function of T,R^1
for r being real positive number holds
( f,the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace (- r),r) )

for r being real number
for X being set
for f, g being real-yielding Function st f - g,X is_absolutely_bounded_by r holds
g - f,X is_absolutely_bounded_by r

for T being non empty TopSpace st T is being_T4 holds
for A being closed Subset of T
for f being Function of (T | A),(Closed-Interval-TSpace (- 1),1) st f is continuous holds
ex g being continuous Function of T,(Closed-Interval-TSpace (- 1),1) st g | A = f

for T being non empty TopSpace st ( for A being non empty closed Subset of T
for f being continuous Function of (T | A),(Closed-Interval-TSpace (- 1),1) ex g being continuous Function of T,(Closed-Interval-TSpace (- 1),1) st g | A = f ) holds
T is being_T4