:: FCONT_1 semantic presentation

begin


definition
let f be PartFunc of REAL,REAL;
let x0 be real number ;
predf is_continuous_in x0 means :Def1: :: FCONT_1:def 1
 for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) );
end;

:: deftheorem Def1 defines is_continuous_in FCONT_1:def_1_:_
 for f being PartFunc of REAL,REAL
for x0 being real number holds
( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) );

theorem Th1: :: FCONT_1:1
for X being set
for x0 being real number
for f being PartFunc of REAL,REAL st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
proof
let X be set ; ::_thesis: for x0 being real number
for f being PartFunc of REAL,REAL st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let f be PartFunc of REAL,REAL; ::_thesis: ( x0 in X & f is_continuous_in x0 implies f | X is_continuous_in x0 )
assume that
A1: x0 in X and
A2: f is_continuous_in x0 ; ::_thesis: f | X is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x0 implies ( (f | X) /* s1 is convergent & (f | X) . x0 = lim ((f | X) /* s1) ) )
assume that
A3: rng s1 c= dom (f | X) and
A4: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f | X) /* s1 is convergent & (f | X) . x0 = lim ((f | X) /* s1) )
 dom (f | X) = X /\ (dom f) by RELAT_1:61;
then A5: rng s1 c= dom f by A3, XBOOLE_1:18;
A6: (f | X) /* s1 = f /* s1 by A3, FUNCT_2:117;
hence  (f | X) /* s1 is convergent by A2, A4, A5, Def1; ::_thesis: (f | X) . x0 = lim ((f | X) /* s1)
thus (f | X) . x0 = f . x0 by A1, FUNCT_1:49
.= lim ((f | X) /* s1) by A2, A4, A5, A6, Def1 ; ::_thesis: verum
end;

theorem :: FCONT_1:2
for x0 being real number
for f being PartFunc of REAL,REAL holds
( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )
proof
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL holds
( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )
thus  ( f is_continuous_in x0 implies for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) ) by Def1; ::_thesis: ( ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) ) implies f is_continuous_in x0 )
assume A1: for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) ; ::_thesis: f is_continuous_in x0
let s2 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) )
assume that
A2: rng s2 c= dom f and
A3: ( s2 is convergent & lim s2 = x0 ) ; ::_thesis: ( f /* s2 is convergent & f . x0 = lim (f /* s2) )
now__::_thesis:_(_f_/*_s2_is_convergent_&_f_._x0_=_lim_(f_/*_s2)_)
percases ( ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 or for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ) ;
suppose ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 ; ::_thesis: ( f /* s2 is convergent & f . x0 = lim (f /* s2) )
then consider N being Element of NAT  such that
A4: for m being Element of NAT st N <= m holds
s2 . m = x0 ;
A5: for n being Element of NAT holds (s2 ^\ N) . n = x0
proof
let n be Element of NAT ; ::_thesis: (s2 ^\ N) . n = x0
 s2 . (n + N) = x0 by A4, NAT_1:12;
hence  (s2 ^\ N) . n = x0 by NAT_1:def_3; ::_thesis: verum
end;
A6: f /* (s2 ^\ N) = (f /* s2) ^\ N by A2, VALUED_0:27;
A7: rng (s2 ^\ N) c= rng s2 by VALUED_0:21;
A8: now__::_thesis:_for_p_being_real_number_st_p_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((f_/*_(s2_^\_N))_._m)_-_(f_._x0))_<_p
let p be real number ; ::_thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p )
assume A9: p > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p )
assume  n <= m ; ::_thesis: abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p
abs (((f /* (s2 ^\ N)) . m) - (f . x0)) = abs ((f . ((s2 ^\ N) . m)) - (f . x0)) by A2, A7, FUNCT_2:108, XBOOLE_1:1
.= abs ((f . x0) - (f . x0)) by A5
.= 0 by ABSVALUE:2 ;
hence  abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p by A9; ::_thesis: verum
end;
then A10: f /* (s2 ^\ N) is convergent by SEQ_2:def_6;
then  f . x0 = lim ((f /* s2) ^\ N) by A8, A6, SEQ_2:def_7;
hence  ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) by A10, A6, SEQ_4:20, SEQ_4:21; ::_thesis: verum
end;
supposeA11: for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ; ::_thesis: ( f /* s2 is convergent & f . x0 = lim (f /* s2) )
defpred S1[ Element of NAT , set , set ] means  for n, m being Element of NAT st $2 = n & $3 = m holds
( n < m & s2 . m <> x0 & ( for k being Element of NAT st n < k & s2 . k <> x0 holds
m <= k ) );
defpred S2[ set ] means s2 . $1 <> x0;
 ex m1 being Element of NAT st
( 0 <= m1 & s2 . m1 <> x0 ) by A11;
then A12: ex m being Nat st S2[m] ;
consider M being Nat such that
A13: ( S2[M] & ( for n being Nat st S2[n] holds
M <= n ) ) from NAT_1:sch_5(A12);
reconsider M9 = M as Element of NAT by ORDINAL1:def_12;
A14: now__::_thesis:_for_n_being_Element_of_NAT_ex_m_being_Element_of_NAT_st_
(_n_<_m_&_s2_._m_<>_x0_)
let n be Element of NAT ; ::_thesis: ex m being Element of NAT st
( n < m & s2 . m <> x0 )
consider m being Element of NAT  such that
A15: ( n + 1 <= m & s2 . m <> x0 ) by A11;
take m = m; ::_thesis: ( n < m & s2 . m <> x0 )
thus  ( n < m & s2 . m <> x0 ) by A15, NAT_1:13; ::_thesis: verum
end;
A16: for n, x being Element of NAT ex y being Element of NAT st S1[n,x,y]
proof
let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S1[n,x,y]
defpred S3[ Nat] means ( x < $1 & s2 . $1 <> x0 );
 ex m being Element of NAT st S3[m] by A14;
then A17: ex m being Nat st S3[m] ;
consider l being Nat such that
A18: ( S3[l] & ( for k being Nat st S3[k] holds
l <= k ) ) from NAT_1:sch_5(A17);
take  l ; ::_thesis: ( l is Element of REAL & l is Element of NAT & S1[n,x,l] )
 l in NAT by ORDINAL1:def_12;
hence  ( l is Element of REAL & l is Element of NAT & S1[n,x,l] ) by A18; ::_thesis: verum
end;
consider F being Function of NAT,NAT such that
A19: ( F . 0 = M9 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A16);
A20: rng F c= REAL by XBOOLE_1:1;
A21: rng F c= NAT ;
A22: dom F = NAT by FUNCT_2:def_1;
then reconsider F = F as Real_Sequence by A20, RELSET_1:4;
A23: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_Element_of_NAT
let n be Element of NAT ; ::_thesis: F . n is Element of NAT
 F . n in rng F by A22, FUNCT_1:def_3;
hence  F . n is Element of NAT by A21; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_<_F_._(n_+_1)
let n be Element of NAT ; ::_thesis: F . n < F . (n + 1)
 ( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A23;
hence  F . n < F . (n + 1) by A19; ::_thesis: verum
end;
then reconsider F = F as V39() sequence of NAT by SEQM_3:def_6;
A24: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A3, SEQ_4:16, SEQ_4:17;
A25: for n being Element of NAT st s2 . n <> x0 holds
ex m being Element of NAT st F . m = n
proof
defpred S3[ set ] means ( s2 . $1 <> x0 & ( for m being Element of NAT holds F . m <> $1 ) );
assume  ex n being Element of NAT st S3[n] ; ::_thesis: contradiction
then A26: ex n being Nat st S3[n] ;
consider M1 being Nat such that
A27: ( S3[M1] & ( for n being Nat st S3[n] holds
M1 <= n ) ) from NAT_1:sch_5(A26);
defpred S4[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Element of NAT st F . m = $1 );
A28: ex n being Nat st S4[n]
proof
take  M ; ::_thesis: S4[M]
 ( M <= M1 & M <> M1 ) by A13, A19, A27;
hence  M < M1 by XXREAL_0:1; ::_thesis: ( s2 . M <> x0 & ex m being Element of NAT st F . m = M )
thus  s2 . M <> x0 by A13; ::_thesis: ex m being Element of NAT st F . m = M
take  0 ; ::_thesis: F . 0 = M
thus  F . 0 = M by A19; ::_thesis: verum
end;
A29: for n being Nat st S4[n] holds
n <= M1 ;
consider MX being Nat such that
A30: ( S4[MX] & ( for n being Nat st S4[n] holds
n <= MX ) ) from NAT_1:sch_6(A29, A28);
A31: for k being Element of NAT st MX < k & k < M1 holds
s2 . k = x0
proof
given k being Element of NAT  such that A32: MX < k and
A33: ( k < M1 & s2 . k <> x0 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ;
suppose ex m being Element of NAT st F . m = k ; ::_thesis: contradiction
hence  contradiction by A30, A32, A33; ::_thesis: verum
end;
suppose for m being Element of NAT holds F . m <> k ; ::_thesis: contradiction
hence  contradiction by A27, A33; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
consider m being Element of NAT  such that
A34: F . m = MX by A30;
A35: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A19, A34;
 M1 in NAT by ORDINAL1:def_12;
then A36: F . (m + 1) <= M1 by A19, A27, A30, A34;
now__::_thesis:_not_F_._(m_+_1)_<>_M1
assume  F . (m + 1) <> M1 ; ::_thesis: contradiction
then  F . (m + 1) < M1 by A36, XXREAL_0:1;
hence  contradiction by A31, A35; ::_thesis: verum
end;
hence  contradiction by A27; ::_thesis: verum
end;
A37: for n being Element of NAT holds (s2 * F) . n <> x0
proof
defpred S3[ Element of NAT ] means (s2 * F) . $1 <> x0;
A38: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume  (s2 * F) . k <> x0 ; ::_thesis: S3[k + 1]
 S1[k,F . k,F . (k + 1)] by A19;
then  s2 . (F . (k + 1)) <> x0 ;
hence  S3[k + 1] by FUNCT_2:15; ::_thesis: verum
end;
A39: S3[ 0 ] by A13, A19, FUNCT_2:15;
thus  for n being Element of NAT holds S3[n] from NAT_1:sch_1(A39, A38); ::_thesis: verum
end;
A40: rng (s2 * F) c= rng s2 by VALUED_0:21;
then  rng (s2 * F) c= dom f by A2, XBOOLE_1:1;
then A41: ( f /* (s2 * F) is convergent & f . x0 = lim (f /* (s2 * F)) ) by A1, A37, A24;
A42: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_(((f_/*_s2)_._m)_-_(f_._x0))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((f /* s2) . m) - (f . x0)) < p )
assume A43: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((f /* s2) . m) - (f . x0)) < p
then consider n being Element of NAT  such that
A44: for m being Element of NAT st n <= m holds
abs (((f /* (s2 * F)) . m) - (f . x0)) < p by A41, SEQ_2:def_7;
take k = F . n; ::_thesis: for m being Element of NAT st k <= m holds
abs (((f /* s2) . m) - (f . x0)) < p
let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((f /* s2) . m) - (f . x0)) < p )
assume A45: k <= m ; ::_thesis: abs (((f /* s2) . m) - (f . x0)) < p
now__::_thesis:_abs_(((f_/*_s2)_._m)_-_(f_._x0))_<_p
percases ( s2 . m = x0 or s2 . m <> x0 ) ;
suppose s2 . m = x0 ; ::_thesis: abs (((f /* s2) . m) - (f . x0)) < p
then  abs (((f /* s2) . m) - (f . x0)) = abs ((f . x0) - (f . x0)) by A2, FUNCT_2:108
.= 0 by ABSVALUE:2 ;
hence  abs (((f /* s2) . m) - (f . x0)) < p by A43; ::_thesis: verum
end;
suppose s2 . m <> x0 ; ::_thesis: abs (((f /* s2) . m) - (f . x0)) < p
then consider l being Element of NAT  such that
A46: m = F . l by A25;
 n <= l by A45, A46, SEQM_3:1;
then  abs (((f /* (s2 * F)) . l) - (f . x0)) < p by A44;
then  abs ((f . ((s2 * F) . l)) - (f . x0)) < p by A2, A40, FUNCT_2:108, XBOOLE_1:1;
then  abs ((f . (s2 . m)) - (f . x0)) < p by A46, FUNCT_2:15;
hence  abs (((f /* s2) . m) - (f . x0)) < p by A2, FUNCT_2:108; ::_thesis: verum
end;
end;
end;
hence  abs (((f /* s2) . m) - (f . x0)) < p ; ::_thesis: verum
end;
hence  f /* s2 is convergent by SEQ_2:def_6; ::_thesis: f . x0 = lim (f /* s2)
hence  f . x0 = lim (f /* s2) by A42, SEQ_2:def_7; ::_thesis: verum
end;
end;
end;
hence  ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) ; ::_thesis: verum
end;

theorem Th3: :: FCONT_1:3
for x0 being real number
for f being PartFunc of REAL,REAL holds
( f is_continuous_in x0 iff for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
proof
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL holds
( f is_continuous_in x0 iff for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_continuous_in x0 iff for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
thus  ( f is_continuous_in x0 implies for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ) ::_thesis: ( ( for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ) implies f is_continuous_in x0 )
proof
assume A1: f is_continuous_in x0 ; ::_thesis: for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
given r being real number  such that A2: 0 < r and
A3: for s being real number holds
( not 0 < s or ex x1 being real number st
( x1 in dom f & abs (x1 - x0) < s & not abs ((f . x1) - (f . x0)) < r ) ) ; ::_thesis: contradiction
defpred S1[ Element of NAT , real number ] means ( $2 in dom f & abs ($2 - x0) < 1 / ($1 + 1) & not abs ((f . $2) - (f . x0)) < r );
A4: for n being Element of NAT ex p being Real st S1[n,p]
proof
let n be Element of NAT ; ::_thesis: ex p being Real st S1[n,p]
 0 < (n + 1) " ;
then  0 < 1 / (n + 1) by XCMPLX_1:215;
then consider p being real number  such that
A5: ( p in dom f & abs (p - x0) < 1 / (n + 1) & not abs ((f . p) - (f . x0)) < r ) by A3;
take  p ; ::_thesis: ( p is Real & S1[n,p] )
thus  ( p is Real & S1[n,p] ) by A5; ::_thesis: verum
end;
consider s1 being Real_Sequence such that
A6: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A4);
A7: rng s1 c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s1 or x in dom f )
assume  x in rng s1 ; ::_thesis: x in dom f
then  ex n being Element of NAT st x = s1 . n by FUNCT_2:113;
hence  x in dom f by A6; ::_thesis: verum
end;
A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_abs_(((f_/*_s1)_._n)_-_(f_._x0))_<_r
let n be Element of NAT ; ::_thesis: not abs (((f /* s1) . n) - (f . x0)) < r
 not abs ((f . (s1 . n)) - (f . x0)) < r by A6;
hence  not abs (((f /* s1) . n) - (f . x0)) < r by A7, FUNCT_2:108; ::_thesis: verum
end;
A9: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((s1_._m)_-_x0)_<_s
let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((s1 . m) - x0) < s )
assume A10: 0 < s ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((s1 . m) - x0) < s
consider n being Element of NAT  such that
A11: s " < n by SEQ_4:3;
 (s ") + 0 < n + 1 by A11, XREAL_1:8;
then  1 / (n + 1) < 1 / (s ") by A10, XREAL_1:76;
then A12: 1 / (n + 1) < s by XCMPLX_1:216;
take k = n; ::_thesis: for m being Element of NAT st k <= m holds
abs ((s1 . m) - x0) < s
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((s1 . m) - x0) < s )
assume  k <= m ; ::_thesis: abs ((s1 . m) - x0) < s
then  k + 1 <= m + 1 by XREAL_1:6;
then  1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
then  1 / (m + 1) < s by A12, XXREAL_0:2;
hence  abs ((s1 . m) - x0) < s by A6, XXREAL_0:2; ::_thesis: verum
end;
then A13: s1 is convergent by SEQ_2:def_6;
then  lim s1 = x0 by A9, SEQ_2:def_7;
then  ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A1, A7, A13, Def1;
then consider n being Element of NAT  such that
A14: for m being Element of NAT st n <= m holds
abs (((f /* s1) . m) - (f . x0)) < r by A2, SEQ_2:def_7;
 abs (((f /* s1) . n) - (f . x0)) < r by A14;
hence  contradiction by A8; ::_thesis: verum
end;
assume A15: for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ; ::_thesis: f is_continuous_in x0
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_f_&_s1_is_convergent_&_lim_s1_=_x0_holds_
(_f_/*_s1_is_convergent_&_f_._x0_=_lim_(f_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 implies ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )
assume that
A16: rng s1 c= dom f and
A17: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( f /* s1 is convergent & f . x0 = lim (f /* s1) )
A18: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_(((f_/*_s1)_._m)_-_(f_._x0))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((f /* s1) . m) - (f . x0)) < p )
assume  0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((f /* s1) . m) - (f . x0)) < p
then consider s being real number  such that
A19: 0 < s and
A20: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < p by A15;
consider n being Element of NAT  such that
A21: for m being Element of NAT st n <= m holds
abs ((s1 . m) - x0) < s by A17, A19, SEQ_2:def_7;
take k = n; ::_thesis: for m being Element of NAT st k <= m holds
abs (((f /* s1) . m) - (f . x0)) < p
let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((f /* s1) . m) - (f . x0)) < p )
assume  k <= m ; ::_thesis: abs (((f /* s1) . m) - (f . x0)) < p
then  ( s1 . m in rng s1 & abs ((s1 . m) - x0) < s ) by A21, VALUED_0:28;
then  abs ((f . (s1 . m)) - (f . x0)) < p by A16, A20;
hence  abs (((f /* s1) . m) - (f . x0)) < p by A16, FUNCT_2:108; ::_thesis: verum
end;
then  f /* s1 is convergent by SEQ_2:def_6;
hence  ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A18, SEQ_2:def_7; ::_thesis: verum
end;
hence  f is_continuous_in x0 by Def1; ::_thesis: verum
end;

theorem Th4: :: FCONT_1:4
for f being PartFunc of REAL,REAL
for x0 being real number holds
( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 )
proof
let f be PartFunc of REAL,REAL; ::_thesis: for x0 being real number holds
( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 )
let x0 be real number ; ::_thesis: ( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 )
thus  ( f is_continuous_in x0 implies for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 ) ::_thesis: ( ( for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 ) implies f is_continuous_in x0 )
proof
assume A1: f is_continuous_in x0 ; ::_thesis: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1
let N1 be Neighbourhood of f . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1
consider r being real number  such that
A2: 0 < r and
A3: N1 = ].((f . x0) - r),((f . x0) + r).[ by RCOMP_1:def_6;
consider s being real number  such that
A4: 0 < s and
A5: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r by A1, A2, Th3;
reconsider N = ].(x0 - s),(x0 + s).[ as Neighbourhood of x0 by A4, RCOMP_1:def_6;
take  N ; ::_thesis: for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1
let x1 be real number ; ::_thesis: ( x1 in dom f & x1 in N implies f . x1 in N1 )
assume that
A6: x1 in dom f and
A7: x1 in N ; ::_thesis: f . x1 in N1
 abs (x1 - x0) < s by A7, RCOMP_1:1;
then  abs ((f . x1) - (f . x0)) < r by A5, A6;
hence  f . x1 in N1 by A3, RCOMP_1:1; ::_thesis: verum
end;
assume A8: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 ; ::_thesis: f is_continuous_in x0
now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1_being_real_number_st_x1_in_dom_f_&_abs_(x1_-_x0)_<_s_holds_
abs_((f_._x1)_-_(f_._x0))_<_r_)_)
let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
assume  0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
then reconsider N1 = ].((f . x0) - r),((f . x0) + r).[ as Neighbourhood of f . x0 by RCOMP_1:def_6;
consider N2 being Neighbourhood of x0 such that
A9: for x1 being real number st x1 in dom f & x1 in N2 holds
f . x1 in N1 by A8;
consider s being real number  such that
A10: 0 < s and
A11: N2 = ].(x0 - s),(x0 + s).[ by RCOMP_1:def_6;
take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
 for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r
proof
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r )
assume that
A12: x1 in dom f and
A13: abs (x1 - x0) < s ; ::_thesis: abs ((f . x1) - (f . x0)) < r
 x1 in N2 by A11, A13, RCOMP_1:1;
then  f . x1 in N1 by A9, A12;
hence  abs ((f . x1) - (f . x0)) < r by RCOMP_1:1; ::_thesis: verum
end;
hence  ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) by A10; ::_thesis: verum
end;
hence  f is_continuous_in x0 by Th3; ::_thesis: verum
end;

theorem Th5: :: FCONT_1:5
for f being PartFunc of REAL,REAL
for x0 being real number holds
( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )
proof
let f be PartFunc of REAL,REAL; ::_thesis: for x0 being real number holds
( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )
let x0 be real number ; ::_thesis: ( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )
thus  ( f is_continuous_in x0 implies for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ::_thesis: ( ( for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) implies f is_continuous_in x0 )
proof
assume A1: f is_continuous_in x0 ; ::_thesis: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1
let N1 be Neighbourhood of f . x0; ::_thesis: ex N being Neighbourhood of x0 st f .: N c= N1
consider N being Neighbourhood of x0 such that
A2: for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1 by A1, Th4;
take  N ; ::_thesis: f .: N c= N1
now__::_thesis:_for_r_being_real_number_st_r_in_f_.:_N_holds_
r_in_N1
let r be real number ; ::_thesis: ( r in f .: N implies r in N1 )
assume  r in f .: N ; ::_thesis: r in N1
then  ex x being Element of REAL st
( x in dom f & x in N & r = f . x ) by PARTFUN2:59;
hence  r in N1 by A2; ::_thesis: verum
end;
hence  f .: N c= N1 by MEMBERED:def_9; ::_thesis: verum
end;
assume A3: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ; ::_thesis: f is_continuous_in x0
now__::_thesis:_for_N1_being_Neighbourhood_of_f_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x1_being_real_number_st_x1_in_dom_f_&_x1_in_N_holds_
f_._x1_in_N1
let N1 be Neighbourhood of f . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1
consider N being Neighbourhood of x0 such that
A4: f .: N c= N1 by A3;
take N = N; ::_thesis: for x1 being real number st x1 in dom f & x1 in N holds
f . x1 in N1
let x1 be real number ; ::_thesis: ( x1 in dom f & x1 in N implies f . x1 in N1 )
assume  ( x1 in dom f & x1 in N ) ; ::_thesis: f . x1 in N1
then  f . x1 in f .: N by FUNCT_1:def_6;
hence  f . x1 in N1 by A4; ::_thesis: verum
end;
hence  f is_continuous_in x0 by Th4; ::_thesis: verum
end;

theorem :: FCONT_1:6
for x0 being real number
for f being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
proof
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
let f be PartFunc of REAL,REAL; ::_thesis: ( ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} implies f is_continuous_in x0 )
given N being Neighbourhood of x0 such that A1: (dom f) /\ N = {x0} ; ::_thesis: f is_continuous_in x0
 x0 in (dom f) /\ N by A1, TARSKI:def_1;
then A2: x0 in dom f by XBOOLE_0:def_4;
now__::_thesis:_for_N1_being_Neighbourhood_of_f_._x0_ex_N_being_Neighbourhood_of_x0_st_f_.:_N_c=_N1
let N1 be Neighbourhood of f . x0; ::_thesis: ex N being Neighbourhood of x0 st f .: N c= N1
take N = N; ::_thesis: f .: N c= N1
A3: f . x0 in N1 by RCOMP_1:16;
f .: N = Im (f,x0) by A1, RELAT_1:112
.= {(f . x0)} by A2, FUNCT_1:59 ;
hence  f .: N c= N1 by A3, ZFMISC_1:31; ::_thesis: verum
end;
hence  f is_continuous_in x0 by Th5; ::_thesis: verum
end;

theorem Th7: :: FCONT_1:7
for x0 being real number
for f1, f2 being PartFunc of REAL,REAL st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
proof
let x0 be real number ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 ) )
assume A1: x0 in (dom f1) /\ (dom f2) ; ::_thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in x0 or ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 ) )
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in x0 ; ::_thesis: ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f1_+_f2)_&_s1_is_convergent_&_lim_s1_=_x0_holds_
(_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_._x0_=_lim_((f1_+_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) . x0 = lim ((f1 + f2) /* s1) ) )
assume that
A4: rng s1 c= dom (f1 + f2) and
A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) . x0 = lim ((f1 + f2) /* s1) )
A6: rng s1 c= (dom f1) /\ (dom f2) by A4, VALUED_1:def_1;
 dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1;
then  dom (f1 + f2) c= dom f2 by XBOOLE_1:17;
then A7: rng s1 c= dom f2 by A4, XBOOLE_1:1;
then A8: f2 /* s1 is convergent by A3, A5, Def1;
 dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1;
then  dom (f1 + f2) c= dom f1 by XBOOLE_1:17;
then A9: rng s1 c= dom f1 by A4, XBOOLE_1:1;
then A10: f1 /* s1 is convergent by A2, A5, Def1;
then  (f1 /* s1) + (f2 /* s1) is convergent by A8;
hence  (f1 + f2) /* s1 is convergent by A6, RFUNCT_2:8; ::_thesis: (f1 + f2) . x0 = lim ((f1 + f2) /* s1)
A11: f1 . x0 = lim (f1 /* s1) by A2, A5, A9, Def1;
A12: f2 . x0 = lim (f2 /* s1) by A3, A5, A7, Def1;
 x0 in dom (f1 + f2) by A1, VALUED_1:def_1;
hence (f1 + f2) . x0 = (f1 . x0) + (f2 . x0) by VALUED_1:def_1
.= lim ((f1 /* s1) + (f2 /* s1)) by A10, A11, A8, A12, SEQ_2:6
.= lim ((f1 + f2) /* s1) by A6, RFUNCT_2:8 ;
::_thesis: verum
end;
hence  f1 + f2 is_continuous_in x0 by Def1; ::_thesis: ( f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f1_-_f2)_&_s1_is_convergent_&_lim_s1_=_x0_holds_
(_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_._x0_=_lim_((f1_-_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) . x0 = lim ((f1 - f2) /* s1) ) )
assume that
A13: rng s1 c= dom (f1 - f2) and
A14: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) . x0 = lim ((f1 - f2) /* s1) )
A15: rng s1 c= (dom f1) /\ (dom f2) by A13, VALUED_1:12;
 dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:12;
then  dom (f1 - f2) c= dom f2 by XBOOLE_1:17;
then A16: rng s1 c= dom f2 by A13, XBOOLE_1:1;
then A17: f2 /* s1 is convergent by A3, A14, Def1;
 dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:12;
then  dom (f1 - f2) c= dom f1 by XBOOLE_1:17;
then A18: rng s1 c= dom f1 by A13, XBOOLE_1:1;
then A19: f1 /* s1 is convergent by A2, A14, Def1;
then  (f1 /* s1) - (f2 /* s1) is convergent by A17;
hence  (f1 - f2) /* s1 is convergent by A15, RFUNCT_2:8; ::_thesis: (f1 - f2) . x0 = lim ((f1 - f2) /* s1)
A20: f1 . x0 = lim (f1 /* s1) by A2, A14, A18, Def1;
A21: f2 . x0 = lim (f2 /* s1) by A3, A14, A16, Def1;
 x0 in dom (f1 - f2) by A1, VALUED_1:12;
hence (f1 - f2) . x0 = (f1 . x0) - (f2 . x0) by VALUED_1:13
.= lim ((f1 /* s1) - (f2 /* s1)) by A19, A20, A17, A21, SEQ_2:12
.= lim ((f1 - f2) /* s1) by A15, RFUNCT_2:8 ;
::_thesis: verum
end;
hence  f1 - f2 is_continuous_in x0 by Def1; ::_thesis: f1 (#) f2 is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = x0 implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . x0 = lim ((f1 (#) f2) /* s1) ) )
assume that
A22: rng s1 c= dom (f1 (#) f2) and
A23: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . x0 = lim ((f1 (#) f2) /* s1) )
 dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  dom (f1 (#) f2) c= dom f2 by XBOOLE_1:17;
then A24: rng s1 c= dom f2 by A22, XBOOLE_1:1;
then A25: f2 /* s1 is convergent by A3, A23, Def1;
A26: rng s1 c= (dom f1) /\ (dom f2) by A22, VALUED_1:def_4;
 dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  dom (f1 (#) f2) c= dom f1 by XBOOLE_1:17;
then A27: rng s1 c= dom f1 by A22, XBOOLE_1:1;
then A28: f1 /* s1 is convergent by A2, A23, Def1;
then  (f1 /* s1) (#) (f2 /* s1) is convergent by A25;
hence  (f1 (#) f2) /* s1 is convergent by A26, RFUNCT_2:8; ::_thesis: (f1 (#) f2) . x0 = lim ((f1 (#) f2) /* s1)
A29: f1 . x0 = lim (f1 /* s1) by A2, A23, A27, Def1;
A30: f2 . x0 = lim (f2 /* s1) by A3, A23, A24, Def1;
thus (f1 (#) f2) . x0 = (f1 . x0) * (f2 . x0) by VALUED_1:5
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A28, A29, A25, A30, SEQ_2:15
.= lim ((f1 (#) f2) /* s1) by A26, RFUNCT_2:8 ; ::_thesis: verum
end;

theorem Th8: :: FCONT_1:8
for x0, r being real number
for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds
r (#) f is_continuous_in x0
proof
let x0, r be real number ; ::_thesis: for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let f be PartFunc of REAL,REAL; ::_thesis: ( x0 in dom f & f is_continuous_in x0 implies r (#) f is_continuous_in x0 )
assume  x0 in dom f ; ::_thesis: ( not f is_continuous_in x0 or r (#) f is_continuous_in x0 )
then A1: x0 in dom (r (#) f) by VALUED_1:def_5;
assume A2: f is_continuous_in x0 ; ::_thesis: r (#) f is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( rng s1 c= dom (r (#) f) & s1 is convergent & lim s1 = x0 implies ( (r (#) f) /* s1 is convergent & (r (#) f) . x0 = lim ((r (#) f) /* s1) ) )
assume that
A3: rng s1 c= dom (r (#) f) and
A4: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) . x0 = lim ((r (#) f) /* s1) )
A5: rng s1 c= dom f by A3, VALUED_1:def_5;
then A6: f . x0 = lim (f /* s1) by A2, A4, Def1;
A7: f /* s1 is convergent by A2, A4, A5, Def1;
then  r (#) (f /* s1) is convergent ;
hence  (r (#) f) /* s1 is convergent by A5, RFUNCT_2:9; ::_thesis: (r (#) f) . x0 = lim ((r (#) f) /* s1)
thus (r (#) f) . x0 = r * (f . x0) by A1, VALUED_1:def_5
.= lim (r (#) (f /* s1)) by A7, A6, SEQ_2:8
.= lim ((r (#) f) /* s1) by A5, RFUNCT_2:9 ; ::_thesis: verum
end;

theorem :: FCONT_1:9
for x0 being real number
for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds
( abs f is_continuous_in x0 & - f is_continuous_in x0 )
proof
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds
( abs f is_continuous_in x0 & - f is_continuous_in x0 )
let f be PartFunc of REAL,REAL; ::_thesis: ( x0 in dom f & f is_continuous_in x0 implies ( abs f is_continuous_in x0 & - f is_continuous_in x0 ) )
assume A1: x0 in dom f ; ::_thesis: ( not f is_continuous_in x0 or ( abs f is_continuous_in x0 & - f is_continuous_in x0 ) )
assume A2: f is_continuous_in x0 ; ::_thesis: ( abs f is_continuous_in x0 & - f is_continuous_in x0 )
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(abs_f)_&_s1_is_convergent_&_lim_s1_=_x0_holds_
(_(abs_f)_/*_s1_is_convergent_&_(abs_f)_._x0_=_lim_((abs_f)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (abs f) & s1 is convergent & lim s1 = x0 implies ( (abs f) /* s1 is convergent & (abs f) . x0 = lim ((abs f) /* s1) ) )
assume that
A3: rng s1 c= dom (abs f) and
A4: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (abs f) /* s1 is convergent & (abs f) . x0 = lim ((abs f) /* s1) )
A5: rng s1 c= dom f by A3, VALUED_1:def_11;
then A6: f . x0 = lim (f /* s1) by A2, A4, Def1;
A7: f /* s1 is convergent by A2, A4, A5, Def1;
then  abs (f /* s1) is convergent by SEQ_4:13;
hence  (abs f) /* s1 is convergent by A5, RFUNCT_2:10; ::_thesis: (abs f) . x0 = lim ((abs f) /* s1)
thus (abs f) . x0 = abs (f . x0) by VALUED_1:18
.= lim (abs (f /* s1)) by A7, A6, SEQ_4:14
.= lim ((abs f) /* s1) by A5, RFUNCT_2:10 ; ::_thesis: verum
end;
hence  abs f is_continuous_in x0 by Def1; ::_thesis: - f is_continuous_in x0
thus  - f is_continuous_in x0 by A1, A2, Th8; ::_thesis: verum
end;

theorem Th10: :: FCONT_1:10
for x0 being real number
for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> 0 holds
f ^ is_continuous_in x0
proof
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> 0 holds
f ^ is_continuous_in x0
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_continuous_in x0 & f . x0 <> 0 implies f ^ is_continuous_in x0 )
assume that
A1: f is_continuous_in x0 and
A2: f . x0 <> 0 ; ::_thesis: f ^ is_continuous_in x0
 not f . x0 in {0} by A2, TARSKI:def_1;
then A3: not x0 in f " {0} by FUNCT_1:def_7;
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( rng s1 c= dom (f ^) & s1 is convergent & lim s1 = x0 implies ( (f ^) /* s1 is convergent & (f ^) . x0 = lim ((f ^) /* s1) ) )
assume that
A4: rng s1 c= dom (f ^) and
A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f ^) /* s1 is convergent & (f ^) . x0 = lim ((f ^) /* s1) )
 ( (dom f) \ (f " {0}) c= dom f & rng s1 c= (dom f) \ (f " {0}) ) by A4, RFUNCT_1:def_2, XBOOLE_1:36;
then  rng s1 c= dom f by XBOOLE_1:1;
then A6: ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A1, A5, Def1;
then  (f /* s1) " is convergent by A2, A4, RFUNCT_2:11, SEQ_2:21;
hence  (f ^) /* s1 is convergent by A4, RFUNCT_2:12; ::_thesis: (f ^) . x0 = lim ((f ^) /* s1)
 x0 in dom f by A2, FUNCT_1:def_2;
then  x0 in (dom f) \ (f " {0}) by A3, XBOOLE_0:def_5;
then  x0 in dom (f ^) by RFUNCT_1:def_2;
hence (f ^) . x0 = (f . x0) " by RFUNCT_1:def_2
.= lim ((f /* s1) ") by A2, A4, A6, RFUNCT_2:11, SEQ_2:22
.= lim ((f ^) /* s1) by A4, RFUNCT_2:12 ;
::_thesis: verum
end;

theorem :: FCONT_1:11
for x0 being real number
for f2, f1 being PartFunc of REAL,REAL st x0 in dom f2 & f1 is_continuous_in x0 & f1 . x0 <> 0 & f2 is_continuous_in x0 holds
f2 / f1 is_continuous_in x0
proof
let x0 be real number ; ::_thesis: for f2, f1 being PartFunc of REAL,REAL st x0 in dom f2 & f1 is_continuous_in x0 & f1 . x0 <> 0 & f2 is_continuous_in x0 holds
f2 / f1 is_continuous_in x0
let f2, f1 be PartFunc of REAL,REAL; ::_thesis: ( x0 in dom f2 & f1 is_continuous_in x0 & f1 . x0 <> 0 & f2 is_continuous_in x0 implies f2 / f1 is_continuous_in x0 )
assume A1: x0 in dom f2 ; ::_thesis: ( not f1 is_continuous_in x0 or not f1 . x0 <> 0 or not f2 is_continuous_in x0 or f2 / f1 is_continuous_in x0 )
assume that
A2: f1 is_continuous_in x0 and
A3: f1 . x0 <> 0 and
A4: f2 is_continuous_in x0 ; ::_thesis: f2 / f1 is_continuous_in x0
 not f1 . x0 in {0} by A3, TARSKI:def_1;
then A5: not x0 in f1 " {0} by FUNCT_1:def_7;
 x0 in dom f1 by A3, FUNCT_1:def_2;
then  x0 in (dom f1) \ (f1 " {0}) by A5, XBOOLE_0:def_5;
then  x0 in dom (f1 ^) by RFUNCT_1:def_2;
then A6: x0 in (dom (f1 ^)) /\ (dom f2) by A1, XBOOLE_0:def_4;
 f1 ^ is_continuous_in x0 by A2, A3, Th10;
then  f2 (#) (f1 ^) is_continuous_in x0 by A4, A6, Th7;
hence  f2 / f1 is_continuous_in x0 by RFUNCT_1:31; ::_thesis: verum
end;

theorem Th12: :: FCONT_1:12
for x0 being real number
for f2, f1 being PartFunc of REAL,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 . x0 holds
f2 * f1 is_continuous_in x0
proof
let x0 be real number ; ::_thesis: for f2, f1 being PartFunc of REAL,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 . x0 holds
f2 * f1 is_continuous_in x0
let f2, f1 be PartFunc of REAL,REAL; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 . x0 implies f2 * f1 is_continuous_in x0 )
assume A1: x0 in dom (f2 * f1) ; ::_thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 . x0 or f2 * f1 is_continuous_in x0 )
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1 . x0 ; ::_thesis: f2 * f1 is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( rng s1 c= dom (f2 * f1) & s1 is convergent & lim s1 = x0 implies ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) ) )
assume that
A4: rng s1 c= dom (f2 * f1) and
A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) )
A6: dom (f2 * f1) c= dom f1 by RELAT_1:25;
now__::_thesis:_for_x_being_set_st_x_in_rng_(f1_/*_s1)_holds_
x_in_dom_f2
let x be set ; ::_thesis: ( x in rng (f1 /* s1) implies x in dom f2 )
assume  x in rng (f1 /* s1) ; ::_thesis: x in dom f2
then consider n being Element of NAT  such that
A7: x = (f1 /* s1) . n by FUNCT_2:113;
 s1 . n in rng s1 by VALUED_0:28;
then  f1 . (s1 . n) in dom f2 by A4, FUNCT_1:11;
hence  x in dom f2 by A4, A6, A7, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum
end;
then A8: rng (f1 /* s1) c= dom f2 by TARSKI:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((f2_*_f1)_/*_s1)_._n_=_(f2_/*_(f1_/*_s1))_._n
let n be Element of NAT ; ::_thesis: ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n
 s1 . n in rng s1 by VALUED_0:28;
then A9: s1 . n in dom f1 by A4, FUNCT_1:11;
thus ((f2 * f1) /* s1) . n = (f2 * f1) . (s1 . n) by A4, FUNCT_2:108
.= f2 . (f1 . (s1 . n)) by A9, FUNCT_1:13
.= f2 . ((f1 /* s1) . n) by A4, A6, FUNCT_2:108, XBOOLE_1:1
.= (f2 /* (f1 /* s1)) . n by A8, FUNCT_2:108 ; ::_thesis: verum
end;
then A10: f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:63;
 rng s1 c= dom f1 by A4, A6, XBOOLE_1:1;
then A11: ( f1 /* s1 is convergent & f1 . x0 = lim (f1 /* s1) ) by A2, A5, Def1;
then  f2 . (f1 . x0) = lim (f2 /* (f1 /* s1)) by A3, A8, Def1;
hence  ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) ) by A1, A3, A11, A8, A10, Def1, FUNCT_1:12; ::_thesis: verum
end;

definition
let f be PartFunc of REAL,REAL;
attrf is continuous  means :Def2: :: FCONT_1:def 2
 for x0 being real number st x0 in dom f holds
f is_continuous_in x0;
end;

:: deftheorem Def2 defines continuous FCONT_1:def_2_:_
 for f being PartFunc of REAL,REAL holds
( f is continuous iff for x0 being real number st x0 in dom f holds
f is_continuous_in x0 );

theorem Th13: :: FCONT_1:13
for X being set
for f being PartFunc of REAL,REAL st X c= dom f holds
( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f holds
( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f implies ( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ) )
assume A1: X c= dom f ; ::_thesis: ( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )
thus  ( f | X is continuous implies for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ) ::_thesis: ( ( for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ) implies f | X is continuous )
proof
assume A2: f | X is continuous ; ::_thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) )
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_f_/*_s1_is_convergent_&_f_._(lim_s1)_=_lim_(f_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )
assume that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X ; ::_thesis: ( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) )
A6: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
then A7: f | X is_continuous_in lim s1 by A2, A5, Def2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_(f_/*_s1)_._n
let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = (f /* s1) . n
A8: s1 . n in rng s1 by VALUED_0:28;
thus ((f | X) /* s1) . n = (f | X) . (s1 . n) by A3, A6, FUNCT_2:108
.= f . (s1 . n) by A3, A6, A8, FUNCT_1:47
.= (f /* s1) . n by A1, A3, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum
end;
then A9: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
f . (lim s1) = (f | X) . (lim s1) by A5, A6, FUNCT_1:47
.= lim (f /* s1) by A3, A4, A6, A7, A9, Def1 ;
hence  ( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) by A3, A4, A6, A7, A9, Def1; ::_thesis: verum
end;
hence  for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ; ::_thesis: verum
end;
assume A10: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ; ::_thesis: f | X is continuous
now__::_thesis:_for_x1_being_real_number_st_x1_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_x1
A11: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
let x1 be real number ; ::_thesis: ( x1 in dom (f | X) implies f | X is_continuous_in x1 )
assume A12: x1 in dom (f | X) ; ::_thesis: f | X is_continuous_in x1
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f_|_X)_&_s1_is_convergent_&_lim_s1_=_x1_holds_
(_(f_|_X)_/*_s1_is_convergent_&_(f_|_X)_._x1_=_lim_((f_|_X)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 implies ( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) ) )
assume that
A13: rng s1 c= dom (f | X) and
A14: s1 is convergent and
A15: lim s1 = x1 ; ::_thesis: ( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_(f_/*_s1)_._n
let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = (f /* s1) . n
A16: s1 . n in rng s1 by VALUED_0:28;
thus ((f | X) /* s1) . n = (f | X) . (s1 . n) by A13, FUNCT_2:108
.= f . (s1 . n) by A13, A16, FUNCT_1:47
.= (f /* s1) . n by A1, A11, A13, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum
end;
then A17: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
(f | X) . (lim s1) = f . (lim s1) by A12, A15, FUNCT_1:47
.= lim ((f | X) /* s1) by A10, A12, A11, A13, A14, A15, A17 ;
hence  ( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) ) by A10, A12, A11, A13, A14, A15, A17; ::_thesis: verum
end;
hence  f | X is_continuous_in x1 by Def1; ::_thesis: verum
end;
hence  f | X is continuous by Def2; ::_thesis: verum
end;

theorem Th14: :: FCONT_1:14
for X being set
for f being PartFunc of REAL,REAL st X c= dom f holds
( f | X is continuous iff for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f holds
( f | X is continuous iff for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f implies ( f | X is continuous iff for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ) )
assume A1: X c= dom f ; ::_thesis: ( f | X is continuous iff for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
thus  ( f | X is continuous implies for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ) ::_thesis: ( ( for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ) implies f | X is continuous )
proof
assume A2: f | X is continuous ; ::_thesis: for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
let x0, r be real number ; ::_thesis: ( x0 in X & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
 x0 in dom (f | X) by A1, A3, RELAT_1:62;
then  f | X is_continuous_in x0 by A2, Def2;
then consider s being real number  such that
A5: 0 < s and
A6: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r by A4, Th3;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
thus  0 < s by A5; ::_thesis: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r
let x1 be real number ; ::_thesis: ( x1 in X & abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r )
assume that
A7: x1 in X and
A8: abs (x1 - x0) < s ; ::_thesis: abs ((f . x1) - (f . x0)) < r
A9: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
then  abs ((f . x1) - (f . x0)) = abs (((f | X) . x1) - (f . x0)) by A7, FUNCT_1:47
.= abs (((f | X) . x1) - ((f | X) . x0)) by A3, A9, FUNCT_1:47 ;
hence  abs ((f . x1) - (f . x0)) < r by A6, A9, A7, A8; ::_thesis: verum
end;
assume A10: for x0, r being real number st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) ; ::_thesis: f | X is continuous
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A11: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
A12: x0 in X by A11;
 for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r ) )
proof
let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r ) ) )
assume  0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r ) )
then consider s being real number  such that
A13: 0 < s and
A14: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r by A10, A12;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r ) )
thus  0 < s by A13; ::_thesis: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
abs (((f | X) . x1) - ((f | X) . x0)) < r
let x1 be real number ; ::_thesis: ( x1 in dom (f | X) & abs (x1 - x0) < s implies abs (((f | X) . x1) - ((f | X) . x0)) < r )
assume that
A15: x1 in dom (f | X) and
A16: abs (x1 - x0) < s ; ::_thesis: abs (((f | X) . x1) - ((f | X) . x0)) < r
abs (((f | X) . x1) - ((f | X) . x0)) = abs (((f | X) . x1) - (f . x0)) by A11, FUNCT_1:47
.= abs ((f . x1) - (f . x0)) by A15, FUNCT_1:47 ;
hence  abs (((f | X) . x1) - ((f | X) . x0)) < r by A14, A15, A16; ::_thesis: verum
end;
hence  f | X is_continuous_in x0 by Th3; ::_thesis: verum
end;
hence  f | X is continuous by Def2; ::_thesis: verum
end;

registration
cluster Function-like V8()  ->  continuous for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st b1 is V8() holds
b1 is continuous
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( f is V8() implies f is continuous )
assume A1: f is V8() ; ::_thesis: f is continuous
now__::_thesis:_for_x0,_r_being_real_number_st_x0_in_dom_f_&_0_<_r_holds_
ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1_being_real_number_st_x1_in_dom_f_&_abs_(x1_-_x0)_<_s_holds_
abs_((f_._x1)_-_(f_._x0))_<_r_)_)
reconsider s = 1 as real number ;
let x0, r be real number ; ::_thesis: ( x0 in dom f & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) ) )
assume that
A2: x0 in dom f and
A3: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
thus  0 < s ; ::_thesis: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r )
assume A4: x1 in dom f ; ::_thesis: ( abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r )
assume  abs (x1 - x0) < s ; ::_thesis: abs ((f . x1) - (f . x0)) < r
 f . x1 = f . x0 by A1, A2, A4, FUNCT_1:def_10;
hence  abs ((f . x1) - (f . x0)) < r by A3, ABSVALUE:2; ::_thesis: verum
end;
then  f | (dom f) is continuous by Th14;
hence  f is continuous ; ::_thesis: verum
end;
end;

registration
cluster Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued continuous for Element of bool [:REAL,REAL:];
existence
 ex b1 being PartFunc of REAL,REAL st b1 is continuous
proof
set f = the V8() PartFunc of REAL,REAL;
take  the V8() PartFunc of REAL,REAL ; ::_thesis: the V8() PartFunc of REAL,REAL is continuous
thus  the V8() PartFunc of REAL,REAL is continuous ; ::_thesis: verum
end;
end;

registration
let f be continuous PartFunc of REAL,REAL;
let X be set ;
clusterf | X ->  continuous for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is continuous
proof
 for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A1: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then  x0 in dom f by RELAT_1:57;
then A2: f is_continuous_in x0 by Def2;
 x0 in X by A1;
hence  f | X is_continuous_in x0 by A2, Th1; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is continuous by Def2; ::_thesis: verum
end;
end;

theorem :: FCONT_1:15
for X being set
for f being PartFunc of REAL,REAL holds
( f | X is continuous iff (f | X) | X is continuous ) ;

theorem Th16: :: FCONT_1:16
for X, X1 being set
for f being PartFunc of REAL,REAL st f | X is continuous & X1 c= X holds
f | X1 is continuous
proof
let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is continuous & X1 c= X holds
f | X1 is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is continuous & X1 c= X implies f | X1 is continuous )
assume A1: f | X is continuous ; ::_thesis: ( not X1 c= X or f | X1 is continuous )
assume  X1 c= X ; ::_thesis: f | X1 is continuous
then  f | X1 = (f | X) | X1 by RELAT_1:74;
hence  f | X1 is continuous by A1; ::_thesis: verum
end;

registration
cluster Function-like empty  ->  continuous for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st b1 is empty holds
b1 is continuous ;
end;

registration
let f be PartFunc of REAL,REAL;
let X be trivial set ;
clusterf | X ->  continuous for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is continuous
proof
percases ( f | X is empty or not f | X is empty ) ;
suppose f | X is empty ; ::_thesis: for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is continuous
hence  for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is continuous ; ::_thesis: verum
end;
suppose not f | X is empty ; ::_thesis: for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is continuous
then consider x0 being real number  such that
A1: x0 in dom (f | X) by MEMBERED:9;
 x0 in X by A1, RELAT_1:57;
then A2: X = {x0} by ZFMISC_1:132;
now__::_thesis:_for_p_being_real_number_st_p_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_p
let p be real number ; ::_thesis: ( p in dom (f | X) implies f | X is_continuous_in p )
assume  p in dom (f | X) ; ::_thesis: f | X is_continuous_in p
then A3: p in {x0} by A2;
thus  f | X is_continuous_in p ::_thesis: verum
proof
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = p implies ( (f | X) /* s1 is convergent & (f | X) . p = lim ((f | X) /* s1) ) )
assume that
A4: rng s1 c= dom (f | X) and
 s1 is convergent and
 lim s1 = p ; ::_thesis: ( (f | X) /* s1 is convergent & (f | X) . p = lim ((f | X) /* s1) )
A5: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17;
 rng s1 c= (dom f) /\ {x0} by A2, A4, RELAT_1:61;
then A6: rng s1 c= {x0} by A5, XBOOLE_1:1;
A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_=_x0
let n be Element of NAT ; ::_thesis: s1 . n = x0
 s1 . n in rng s1 by VALUED_0:28;
hence  s1 . n = x0 by A6, TARSKI:def_1; ::_thesis: verum
end;
A8: p = x0 by A3, TARSKI:def_1;
A9: now__::_thesis:_for_g_being_real_number_st_0_<_g_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((((f_|_{x0})_/*_s1)_._m)_-_((f_|_{x0})_._p))_<_g
let g be real number ; ::_thesis: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g )
assume A10: 0 < g ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g )
assume  n <= m ; ::_thesis: abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g
abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) = abs (((f | {x0}) . (s1 . m)) - ((f | {x0}) . x0)) by A2, A8, A4, FUNCT_2:108
.= abs (((f | {x0}) . x0) - ((f | {x0}) . x0)) by A7
.= 0 by ABSVALUE:2 ;
hence  abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g by A10; ::_thesis: verum
end;
hence  (f | X) /* s1 is convergent by A2, SEQ_2:def_6; ::_thesis: (f | X) . p = lim ((f | X) /* s1)
hence  (f | X) . p = lim ((f | X) /* s1) by A2, A9, SEQ_2:def_7; ::_thesis: verum
end;
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is continuous by Def2; ::_thesis: verum
end;
end;
end;
end;

theorem :: FCONT_1:17
for x0 being real number
for f being PartFunc of REAL,REAL holds f | {x0} is continuous ;

registration
let f1, f2 be continuous PartFunc of REAL,REAL;
clusterf1 + f2 ->  continuous for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f1 + f2 holds
b1 is continuous
proof
set X = dom (f1 + f2);
 dom (f1 + f2) c= (dom f1) /\ (dom f2) by VALUED_1:def_1;
then A1: ( dom (f1 + f2) c= dom f1 & dom (f1 + f2) c= dom f2 ) by XBOOLE_1:18;
A2: ( f1 | (dom (f1 + f2)) is continuous & f2 | (dom (f1 + f2)) is continuous ) ;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f1_+_f2)_&_s1_is_convergent_&_lim_s1_in_dom_(f1_+_f2)_holds_
(_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_._(lim_s1)_=_lim_((f1_+_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 in dom (f1 + f2) implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) ) )
assume that
A3: rng s1 c= dom (f1 + f2) and
A4: s1 is convergent and
A5: lim s1 in dom (f1 + f2) ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) )
A6: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A2, A3, A4, A5, Th13;
then A7: (f1 /* s1) + (f2 /* s1) is convergent ;
A8: rng s1 c= (dom f1) /\ (dom f2) by A3, VALUED_1:def_1;
 ( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A1, A2, A3, A4, A5, Th13;
then (f1 + f2) . (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A5, VALUED_1:def_1
.= lim ((f1 /* s1) + (f2 /* s1)) by A6, SEQ_2:6
.= lim ((f1 + f2) /* s1) by A8, RFUNCT_2:8 ;
hence  ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) ) by A8, A7, RFUNCT_2:8; ::_thesis: verum
end;
then  (f1 + f2) | (dom (f1 + f2)) is continuous by Th13;
hence  for b1 being PartFunc of REAL,REAL st b1 = f1 + f2 holds
b1 is continuous ; ::_thesis: verum
end;
clusterf1 - f2 ->  continuous for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f1 - f2 holds
b1 is continuous
proof
set X = dom (f1 - f2);
 dom (f1 - f2) c= (dom f1) /\ (dom f2) by VALUED_1:12;
then A9: ( dom (f1 - f2) c= dom f1 & dom (f1 - f2) c= dom f2 ) by XBOOLE_1:18;
A10: ( f1 | (dom (f1 - f2)) is continuous & f2 | (dom (f1 - f2)) is continuous ) ;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f1_-_f2)_&_s1_is_convergent_&_lim_s1_in_dom_(f1_-_f2)_holds_
(_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_._(lim_s1)_=_lim_((f1_-_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 in dom (f1 - f2) implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) ) )
assume that
A11: rng s1 c= dom (f1 - f2) and
A12: s1 is convergent and
A13: lim s1 in dom (f1 - f2) ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) )
A14: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A9, A10, A11, A12, A13, Th13;
then A15: (f1 /* s1) - (f2 /* s1) is convergent ;
A16: rng s1 c= (dom f1) /\ (dom f2) by A11, VALUED_1:12;
 ( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A9, A10, A11, A12, A13, Th13;
then (f1 - f2) . (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A13, VALUED_1:13
.= lim ((f1 /* s1) - (f2 /* s1)) by A14, SEQ_2:12
.= lim ((f1 - f2) /* s1) by A16, RFUNCT_2:8 ;
hence  ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) ) by A16, A15, RFUNCT_2:8; ::_thesis: verum
end;
then  (f1 - f2) | (dom (f1 - f2)) is continuous by Th13;
hence  for b1 being PartFunc of REAL,REAL st b1 = f1 - f2 holds
b1 is continuous ; ::_thesis: verum
end;
clusterf1 (#) f2 ->  continuous for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f1 (#) f2 holds
b1 is continuous
proof
set X = dom (f1 (#) f2);
 dom (f1 (#) f2) c= (dom f1) /\ (dom f2) by VALUED_1:def_4;
then A17: ( dom (f1 (#) f2) c= dom f1 & dom (f1 (#) f2) c= dom f2 ) by XBOOLE_1:18;
A18: ( f1 | (dom (f1 (#) f2)) is continuous & f2 | (dom (f1 (#) f2)) is continuous ) ;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f1_(#)_f2)_&_s1_is_convergent_&_lim_s1_in_dom_(f1_(#)_f2)_holds_
(_(f1_(#)_f2)_/*_s1_is_convergent_&_(f1_(#)_f2)_._(lim_s1)_=_lim_((f1_(#)_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 in dom (f1 (#) f2) implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) ) )
assume that
A19: rng s1 c= dom (f1 (#) f2) and
A20: s1 is convergent and
A21: lim s1 in dom (f1 (#) f2) ; ::_thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) )
A22: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A17, A18, A19, A20, A21, Th13;
then A23: (f1 /* s1) (#) (f2 /* s1) is convergent ;
A24: rng s1 c= (dom f1) /\ (dom f2) by A19, VALUED_1:def_4;
 ( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A17, A18, A19, A20, A21, Th13;
then (f1 (#) f2) . (lim s1) = (lim (f1 /* s1)) * (lim (f2 /* s1)) by A21, VALUED_1:def_4
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A22, SEQ_2:15
.= lim ((f1 (#) f2) /* s1) by A24, RFUNCT_2:8 ;
hence  ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) ) by A24, A23, RFUNCT_2:8; ::_thesis: verum
end;
then  (f1 (#) f2) | (dom (f1 (#) f2)) is continuous by Th13;
hence  for b1 being PartFunc of REAL,REAL st b1 = f1 (#) f2 holds
b1 is continuous ; ::_thesis: verum
end;
end;

theorem Th18: :: FCONT_1:18
for X being set
for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )
proof
let X be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous implies ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous ) )
assume A1: X c= (dom f1) /\ (dom f2) ; ::_thesis: ( not f1 | X is continuous or not f2 | X is continuous or ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous ) )
assume A2: ( f1 | X is continuous & f2 | X is continuous ) ; ::_thesis: ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )
A3: ( X c= dom f1 & X c= dom f2 ) by A1, XBOOLE_1:18;
A4: now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(f1_(#)_f2)_/*_s1_is_convergent_&_(f1_(#)_f2)_._(lim_s1)_=_lim_((f1_(#)_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) ) )
assume that
A5: rng s1 c= X and
A6: ( s1 is convergent & lim s1 in X ) ; ::_thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) )
A7: rng s1 c= (dom f1) /\ (dom f2) by A1, A5, XBOOLE_1:1;
A8: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A5, A6, Th13;
then A9: (f1 /* s1) (#) (f2 /* s1) is convergent ;
 ( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A3, A2, A5, A6, Th13;
then (f1 (#) f2) . (lim s1) = (lim (f1 /* s1)) * (lim (f2 /* s1)) by VALUED_1:5
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A8, SEQ_2:15
.= lim ((f1 (#) f2) /* s1) by A7, RFUNCT_2:8 ;
hence  ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) . (lim s1) = lim ((f1 (#) f2) /* s1) ) by A7, A9, RFUNCT_2:8; ::_thesis: verum
end;
A10: X c= dom (f1 + f2) by A1, VALUED_1:def_1;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_._(lim_s1)_=_lim_((f1_+_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) ) )
assume that
A11: rng s1 c= X and
A12: s1 is convergent and
A13: lim s1 in X ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) )
A14: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A11, A12, A13, Th13;
then A15: (f1 /* s1) + (f2 /* s1) is convergent ;
A16: rng s1 c= (dom f1) /\ (dom f2) by A1, A11, XBOOLE_1:1;
 ( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A3, A2, A11, A12, A13, Th13;
then (f1 + f2) . (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A10, A13, VALUED_1:def_1
.= lim ((f1 /* s1) + (f2 /* s1)) by A14, SEQ_2:6
.= lim ((f1 + f2) /* s1) by A16, RFUNCT_2:8 ;
hence  ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) ) by A16, A15, RFUNCT_2:8; ::_thesis: verum
end;
hence  (f1 + f2) | X is continuous by A10, Th13; ::_thesis: ( (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )
A17: X c= dom (f1 - f2) by A1, VALUED_1:12;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_._(lim_s1)_=_lim_((f1_-_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) ) )
assume that
A18: rng s1 c= X and
A19: s1 is convergent and
A20: lim s1 in X ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) )
A21: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A18, A19, A20, Th13;
then A22: (f1 /* s1) - (f2 /* s1) is convergent ;
A23: rng s1 c= (dom f1) /\ (dom f2) by A1, A18, XBOOLE_1:1;
 ( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A3, A2, A18, A19, A20, Th13;
then (f1 - f2) . (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A17, A20, VALUED_1:13
.= lim ((f1 /* s1) - (f2 /* s1)) by A21, SEQ_2:12
.= lim ((f1 - f2) /* s1) by A23, RFUNCT_2:8 ;
hence  ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) ) by A23, A22, RFUNCT_2:8; ::_thesis: verum
end;
hence  (f1 - f2) | X is continuous by A17, Th13; ::_thesis: (f1 (#) f2) | X is continuous
 X c= dom (f1 (#) f2) by A1, VALUED_1:def_4;
hence  (f1 (#) f2) | X is continuous by A4, Th13; ::_thesis: verum
end;

theorem :: FCONT_1:19
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds
( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous & (f1 (#) f2) | (X /\ X1) is continuous )
proof
let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds
( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous & (f1 (#) f2) | (X /\ X1) is continuous )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous implies ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous & (f1 (#) f2) | (X /\ X1) is continuous ) )
assume  ( X c= dom f1 & X1 c= dom f2 ) ; ::_thesis: ( not f1 | X is continuous or not f2 | X1 is continuous or ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous & (f1 (#) f2) | (X /\ X1) is continuous ) )
then A1: X /\ X1 c= (dom f1) /\ (dom f2) by XBOOLE_1:27;
assume  ( f1 | X is continuous & f2 | X1 is continuous ) ; ::_thesis: ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous & (f1 (#) f2) | (X /\ X1) is continuous )
then  ( f1 | (X /\ X1) is continuous & f2 | (X /\ X1) is continuous ) by Th16, XBOOLE_1:17;
hence  ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous & (f1 (#) f2) | (X /\ X1) is continuous ) by A1, Th18; ::_thesis: verum
end;

registration
let f be continuous PartFunc of REAL,REAL;
let r be real number ;
clusterr (#) f ->  continuous for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = r (#) f holds
b1 is continuous
proof
set X = dom f;
A1: dom f c= dom (r (#) f) by VALUED_1:def_5;
A2: f | (dom f) is continuous ;
A3: now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_f_&_s1_is_convergent_&_lim_s1_in_dom_f_holds_
(_(r_(#)_f)_/*_s1_is_convergent_&_(r_(#)_f)_._(lim_s1)_=_lim_((r_(#)_f)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 in dom f implies ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) )
assume that
A4: rng s1 c= dom f and
A5: s1 is convergent and
A6: lim s1 in dom f ; ::_thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )
A7: f /* s1 is convergent by A2, A4, A5, A6, Th13;
then A8: r (#) (f /* s1) is convergent ;
 f . (lim s1) = lim (f /* s1) by A2, A4, A5, A6, Th13;
then (r (#) f) . (lim s1) = r * (lim (f /* s1)) by A1, A6, VALUED_1:def_5
.= lim (r (#) (f /* s1)) by A7, SEQ_2:8
.= lim ((r (#) f) /* s1) by A4, RFUNCT_2:9 ;
hence  ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) by A4, A8, RFUNCT_2:9; ::_thesis: verum
end;
 dom (r (#) f) = dom f by VALUED_1:def_5;
then  (r (#) f) | (dom f) = r (#) f by RELAT_1:69;
hence  for b1 being PartFunc of REAL,REAL st b1 = r (#) f holds
b1 is continuous by A1, A3, Th13; ::_thesis: verum
end;
end;

theorem Th20: :: FCONT_1:20
for r being real number
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
proof
let r be real number ; ::_thesis: for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous )
assume A1: X c= dom f ; ::_thesis: ( not f | X is continuous or (r (#) f) | X is continuous )
assume A2: f | X is continuous ; ::_thesis: (r (#) f) | X is continuous
A3: X c= dom (r (#) f) by A1, VALUED_1:def_5;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(r_(#)_f)_/*_s1_is_convergent_&_(r_(#)_f)_._(lim_s1)_=_lim_((r_(#)_f)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) )
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X ; ::_thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )
A7: f /* s1 is convergent by A1, A2, A4, A5, A6, Th13;
then A8: r (#) (f /* s1) is convergent ;
 f . (lim s1) = lim (f /* s1) by A1, A2, A4, A5, A6, Th13;
then (r (#) f) . (lim s1) = r * (lim (f /* s1)) by A3, A6, VALUED_1:def_5
.= lim (r (#) (f /* s1)) by A7, SEQ_2:8
.= lim ((r (#) f) /* s1) by A1, A4, RFUNCT_2:9, XBOOLE_1:1 ;
hence  ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) by A1, A4, A8, RFUNCT_2:9, XBOOLE_1:1; ::_thesis: verum
end;
hence  (r (#) f) | X is continuous by A3, Th13; ::_thesis: verum
end;

theorem :: FCONT_1:21
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
( (abs f) | X is continuous & (- f) | X is continuous )
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
( (abs f) | X is continuous & (- f) | X is continuous )
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is continuous implies ( (abs f) | X is continuous & (- f) | X is continuous ) )
assume A1: X c= dom f ; ::_thesis: ( not f | X is continuous or ( (abs f) | X is continuous & (- f) | X is continuous ) )
assume A2: f | X is continuous ; ::_thesis: ( (abs f) | X is continuous & (- f) | X is continuous )
thus  (abs f) | X is continuous ::_thesis: (- f) | X is continuous
proof
let r be real number ; :: according to FCONT_1:def_2 ::_thesis: ( r in dom ((abs f) | X) implies (abs f) | X is_continuous_in r )
assume A3: r in dom ((abs f) | X) ; ::_thesis: (abs f) | X is_continuous_in r
then  r in dom (abs f) by RELAT_1:57;
then A4: r in dom f by VALUED_1:def_11;
 r in X by A3;
then A5: r in dom (f | X) by A4, RELAT_1:57;
then A6: f | X is_continuous_in r by A2, Def2;
thus  (abs f) | X is_continuous_in r ::_thesis: verum
proof
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( rng s1 c= dom ((abs f) | X) & s1 is convergent & lim s1 = r implies ( ((abs f) | X) /* s1 is convergent & ((abs f) | X) . r = lim (((abs f) | X) /* s1) ) )
assume that
A7: rng s1 c= dom ((abs f) | X) and
A8: ( s1 is convergent & lim s1 = r ) ; ::_thesis: ( ((abs f) | X) /* s1 is convergent & ((abs f) | X) . r = lim (((abs f) | X) /* s1) )
 rng s1 c= (dom (abs f)) /\ X by A7, RELAT_1:61;
then  rng s1 c= (dom f) /\ X by VALUED_1:def_11;
then A9: rng s1 c= dom (f | X) by RELAT_1:61;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_((f_|_X)_/*_s1))_._n_=_(((abs_f)_|_X)_/*_s1)_._n
let n be Element of NAT ; ::_thesis: (abs ((f | X) /* s1)) . n = (((abs f) | X) /* s1) . n
A10: s1 . n in rng s1 by VALUED_0:28;
then  s1 . n in dom (f | X) by A9;
then  s1 . n in (dom f) /\ X by RELAT_1:61;
then A11: s1 . n in X by XBOOLE_0:def_4;
thus (abs ((f | X) /* s1)) . n = abs (((f | X) /* s1) . n) by SEQ_1:12
.= abs ((f | X) . (s1 . n)) by A9, FUNCT_2:108
.= abs (f . (s1 . n)) by A9, A10, FUNCT_1:47
.= (abs f) . (s1 . n) by VALUED_1:18
.= ((abs f) | X) . (s1 . n) by A11, FUNCT_1:49
.= (((abs f) | X) /* s1) . n by A7, FUNCT_2:108 ; ::_thesis: verum
end;
then A12: abs ((f | X) /* s1) = ((abs f) | X) /* s1 by FUNCT_2:63;
A13: abs ((f | X) . r) = abs (f . r) by A5, FUNCT_1:47
.= (abs f) . r by VALUED_1:18
.= ((abs f) | X) . r by A3, FUNCT_1:47 ;
A14: (f | X) /* s1 is convergent by A6, A8, A9, Def1;
hence  ((abs f) | X) /* s1 is convergent by A12, SEQ_4:13; ::_thesis: ((abs f) | X) . r = lim (((abs f) | X) /* s1)
 (f | X) . r = lim ((f | X) /* s1) by A6, A8, A9, Def1;
hence  ((abs f) | X) . r = lim (((abs f) | X) /* s1) by A14, A12, A13, SEQ_4:14; ::_thesis: verum
end;
end;
thus  (- f) | X is continuous by A1, A2, Th20; ::_thesis: verum
end;

theorem Th22: :: FCONT_1:22
for X being set
for f being PartFunc of REAL,REAL st f | X is continuous & f " {0} = {} holds
(f ^) | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is continuous & f " {0} = {} holds
(f ^) | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is continuous & f " {0} = {} implies (f ^) | X is continuous )
assume that
A1: f | X is continuous and
A2: f " {0} = {} ; ::_thesis: (f ^) | X is continuous
A3: dom (f ^) = (dom f) \ {} by A2, RFUNCT_1:def_2
.= dom f ;
let r be real number ; :: according to FCONT_1:def_2 ::_thesis: ( r in dom ((f ^) | X) implies (f ^) | X is_continuous_in r )
assume A4: r in dom ((f ^) | X) ; ::_thesis: (f ^) | X is_continuous_in r
then A5: r in dom (f ^) by RELAT_1:57;
 r in X by A4;
then A6: r in dom (f | X) by A3, A5, RELAT_1:57;
then A7: f | X is_continuous_in r by A1, Def2;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_((f_^)_|_X)_&_s1_is_convergent_&_lim_s1_=_r_holds_
(_((f_^)_|_X)_/*_s1_is_convergent_&_lim_(((f_^)_|_X)_/*_s1)_=_((f_^)_|_X)_._r_)
A8: now__::_thesis:_not_f_._r_=_0
assume  f . r = 0 ; ::_thesis: contradiction
then  f . r in {0} by TARSKI:def_1;
hence  contradiction by A2, A3, A5, FUNCT_1:def_7; ::_thesis: verum
end;
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom ((f ^) | X) & s1 is convergent & lim s1 = r implies ( ((f ^) | X) /* s1 is convergent & lim (((f ^) | X) /* s1) = ((f ^) | X) . r ) )
assume that
A9: rng s1 c= dom ((f ^) | X) and
A10: ( s1 is convergent & lim s1 = r ) ; ::_thesis: ( ((f ^) | X) /* s1 is convergent & lim (((f ^) | X) /* s1) = ((f ^) | X) . r )
 rng s1 c= (dom (f ^)) /\ X by A9, RELAT_1:61;
then A11: rng s1 c= dom (f | X) by A3, RELAT_1:61;
then A12: (f | X) /* s1 is convergent by A7, A10, Def1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_<>_0
let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n <> 0
A13: s1 . n in rng s1 by VALUED_0:28;
 ( rng s1 c= (dom f) /\ X & (dom f) /\ X c= dom f ) by A3, A9, RELAT_1:61, XBOOLE_1:17;
then A14: rng s1 c= dom f by XBOOLE_1:1;
A15: now__::_thesis:_not_f_._(s1_._n)_=_0
assume  f . (s1 . n) = 0 ; ::_thesis: contradiction
then  f . (s1 . n) in {0} by TARSKI:def_1;
hence  contradiction by A2, A14, A13, FUNCT_1:def_7; ::_thesis: verum
end;
((f | X) /* s1) . n = (f | X) . (s1 . n) by A11, FUNCT_2:108
.= f . (s1 . n) by A11, A13, FUNCT_1:47 ;
hence  ((f | X) /* s1) . n <> 0 by A15; ::_thesis: verum
end;
then A16: (f | X) /* s1 is non-zero by SEQ_1:5;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_^)_|_X)_/*_s1)_._n_=_(((f_|_X)_/*_s1)_")_._n
let n be Element of NAT ; ::_thesis: (((f ^) | X) /* s1) . n = (((f | X) /* s1) ") . n
A17: s1 . n in rng s1 by VALUED_0:28;
then  s1 . n in dom ((f ^) | X) by A9;
then  s1 . n in (dom (f ^)) /\ X by RELAT_1:61;
then A18: s1 . n in dom (f ^) by XBOOLE_0:def_4;
thus (((f ^) | X) /* s1) . n = ((f ^) | X) . (s1 . n) by A9, FUNCT_2:108
.= (f ^) . (s1 . n) by A9, A17, FUNCT_1:47
.= (f . (s1 . n)) " by A18, RFUNCT_1:def_2
.= ((f | X) . (s1 . n)) " by A11, A17, FUNCT_1:47
.= (((f | X) /* s1) . n) " by A11, FUNCT_2:108
.= (((f | X) /* s1) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
then A19: ((f ^) | X) /* s1 = ((f | X) /* s1) " by FUNCT_2:63;
A20: (f | X) . r = f . r by A6, FUNCT_1:47;
then  lim ((f | X) /* s1) <> 0 by A7, A10, A11, A8, Def1;
hence  ((f ^) | X) /* s1 is convergent by A12, A16, A19, SEQ_2:21; ::_thesis: lim (((f ^) | X) /* s1) = ((f ^) | X) . r
 (f | X) . r = lim ((f | X) /* s1) by A7, A10, A11, Def1;
hence  lim (((f ^) | X) /* s1) = ((f | X) . r) " by A12, A20, A8, A16, A19, SEQ_2:22
.= (f . r) " by A6, FUNCT_1:47
.= (f ^) . r by A5, RFUNCT_1:def_2
.= ((f ^) | X) . r by A4, FUNCT_1:47 ;
::_thesis: verum
end;
hence  (f ^) | X is_continuous_in r by Def1; ::_thesis: verum
end;

theorem :: FCONT_1:23
for X being set
for f being PartFunc of REAL,REAL st f | X is continuous & (f | X) " {0} = {} holds
(f ^) | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is continuous & (f | X) " {0} = {} holds
(f ^) | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is continuous & (f | X) " {0} = {} implies (f ^) | X is continuous )
assume that
A1: f | X is continuous and
A2: (f | X) " {0} = {} ; ::_thesis: (f ^) | X is continuous
 (f | X) | X is continuous by A1;
then  ((f | X) ^) | X is continuous by A2, Th22;
then  ((f ^) | X) | X is continuous by RFUNCT_1:46;
hence  (f ^) | X is continuous ; ::_thesis: verum
end;

theorem :: FCONT_1:24
for X being set
for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f1 " {0} = {} & f2 | X is continuous holds
(f2 / f1) | X is continuous
proof
let X be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f1 " {0} = {} & f2 | X is continuous holds
(f2 / f1) | X is continuous
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f1 " {0} = {} & f2 | X is continuous implies (f2 / f1) | X is continuous )
assume A1: X c= (dom f1) /\ (dom f2) ; ::_thesis: ( not f1 | X is continuous or not f1 " {0} = {} or not f2 | X is continuous or (f2 / f1) | X is continuous )
assume that
A2: f1 | X is continuous and
A3: f1 " {0} = {} and
A4: f2 | X is continuous ; ::_thesis: (f2 / f1) | X is continuous
A5: dom (f1 ^) = (dom f1) \ {} by A3, RFUNCT_1:def_2
.= dom f1 ;
 (f1 ^) | X is continuous by A2, A3, Th22;
then  (f2 (#) (f1 ^)) | X is continuous by A1, A4, A5, Th18;
hence  (f2 / f1) | X is continuous by RFUNCT_1:31; ::_thesis: verum
end;

registration
let f1, f2 be continuous PartFunc of REAL,REAL;
clusterf1 (#) f2 ->  continuous for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f2 * f1 holds
b1 is continuous
proof
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_(f2_*_f1)_holds_
f2_*_f1_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom (f2 * f1) implies f2 * f1 is_continuous_in x0 )
assume A1: x0 in dom (f2 * f1) ; ::_thesis: f2 * f1 is_continuous_in x0
then  f1 . x0 in dom f2 by FUNCT_1:11;
then A2: f2 is_continuous_in f1 . x0 by Def2;
 x0 in dom f1 by A1, FUNCT_1:11;
then  f1 is_continuous_in x0 by Def2;
hence  f2 * f1 is_continuous_in x0 by A1, A2, Th12; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = f2 * f1 holds
b1 is continuous by Def2; ::_thesis: verum
end;
end;

theorem :: FCONT_1:25
for X being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | (f1 .: X) is continuous holds
(f2 * f1) | X is continuous
proof
let X be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | (f1 .: X) is continuous holds
(f2 * f1) | X is continuous
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( f1 | X is continuous & f2 | (f1 .: X) is continuous implies (f2 * f1) | X is continuous )
 (f2 * f1) | X = (f2 | (f1 .: X)) * (f1 | X) by FUNCT_1:99;
hence  ( f1 | X is continuous & f2 | (f1 .: X) is continuous implies (f2 * f1) | X is continuous ) ; ::_thesis: verum
end;

theorem :: FCONT_1:26
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | X1 is continuous holds
(f2 * f1) | (X /\ (f1 " X1)) is continuous
proof
let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | X1 is continuous holds
(f2 * f1) | (X /\ (f1 " X1)) is continuous
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( f1 | X is continuous & f2 | X1 is continuous implies (f2 * f1) | (X /\ (f1 " X1)) is continuous )
 (f2 | X1) * (f1 | X) = (f2 * f1) | (X /\ (f1 " X1)) by FUNCT_1:100;
hence  ( f1 | X is continuous & f2 | X1 is continuous implies (f2 * f1) | (X /\ (f1 " X1)) is continuous ) ; ::_thesis: verum
end;

theorem :: FCONT_1:27
for f being PartFunc of REAL,REAL st f is total & ( for x1, x2 being real number holds f . (x1 + x2) = (f . x1) + (f . x2) ) & ex x0 being real number st f is_continuous_in x0 holds
f | REAL is continuous
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( f is total & ( for x1, x2 being real number holds f . (x1 + x2) = (f . x1) + (f . x2) ) & ex x0 being real number st f is_continuous_in x0 implies f | REAL is continuous )
assume that
A1: f is total and
A2: for x1, x2 being real number holds f . (x1 + x2) = (f . x1) + (f . x2) ; ::_thesis: ( for x0 being real number holds not f is_continuous_in x0 or f | REAL is continuous )
A3: dom f = REAL by A1, PARTFUN1:def_2;
given x0 being real number  such that A4: f is_continuous_in x0 ; ::_thesis: f | REAL is continuous
A5: (f . x0) + 0 = f . (x0 + 0)
.= (f . x0) + (f . 0) by A2 ;
A6: now__::_thesis:_for_x1_being_real_number_holds_-_(f_._x1)_=_f_._(-_x1)
let x1 be real number ; ::_thesis: - (f . x1) = f . (- x1)
0 = f . (x1 + (- x1)) by A5
.= (f . x1) + (f . (- x1)) by A2 ;
hence  - (f . x1) = f . (- x1) ; ::_thesis: verum
end;
A7: now__::_thesis:_for_x1,_x2_being_real_number_holds_f_._(x1_-_x2)_=_(f_._x1)_-_(f_._x2)
let x1, x2 be real number ; ::_thesis: f . (x1 - x2) = (f . x1) - (f . x2)
thus f . (x1 - x2) = f . (x1 + (- x2))
.= (f . x1) + (f . (- x2)) by A2
.= (f . x1) + (- (f . x2)) by A6
.= (f . x1) - (f . x2) ; ::_thesis: verum
end;
now__::_thesis:_for_x1,_r_being_real_number_st_x1_in_REAL_&_r_>_0_holds_
ex_s_being_real_number_st_
(_s_>_0_&_(_for_x2_being_real_number_st_x2_in_REAL_&_abs_(x2_-_x1)_<_s_holds_
abs_((f_._x2)_-_(f_._x1))_<_r_)_)
let x1, r be real number ; ::_thesis: ( x1 in REAL & r > 0 implies ex s being real number st
( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
abs ((f . x2) - (f . x1)) < r ) ) )
assume that
 x1 in REAL and
A8: r > 0 ; ::_thesis: ex s being real number st
( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
abs ((f . x2) - (f . x1)) < r ) )
set y = x1 - x0;
consider s being real number  such that
A9: 0 < s and
A10: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r by A4, A8, Th3;
take s = s; ::_thesis: ( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
abs ((f . x2) - (f . x1)) < r ) )
thus  s > 0 by A9; ::_thesis: for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
abs ((f . x2) - (f . x1)) < r
let x2 be real number ; ::_thesis: ( x2 in REAL & abs (x2 - x1) < s implies abs ((f . x2) - (f . x1)) < r )
assume that
 x2 in REAL and
A11: abs (x2 - x1) < s ; ::_thesis: abs ((f . x2) - (f . x1)) < r
A12: ( x2 - (x1 - x0) is Real & abs ((x2 - (x1 - x0)) - x0) = abs (x2 - x1) ) by XREAL_0:def_1;
 (x1 - x0) + x0 = x1 ;
then  abs ((f . x2) - (f . x1)) = abs ((f . x2) - ((f . (x1 - x0)) + (f . x0))) by A2
.= abs (((f . x2) - (f . (x1 - x0))) - (f . x0))
.= abs ((f . (x2 - (x1 - x0))) - (f . x0)) by A7 ;
hence  abs ((f . x2) - (f . x1)) < r by A3, A10, A11, A12; ::_thesis: verum
end;
hence  f | REAL is continuous by A3, Th14; ::_thesis: verum
end;

theorem Th28: :: FCONT_1:28
for f being PartFunc of REAL,REAL st dom f is compact & f | (dom f) is continuous holds
rng f is compact
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( dom f is compact & f | (dom f) is continuous implies rng f is compact )
assume that
A1: dom f is compact and
A2: f | (dom f) is continuous ; ::_thesis: rng f is compact
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_rng_f_holds_
ex_q2_being_Element_of_bool_[:NAT,REAL:]_st_
(_q2_is_subsequence_of_s1_&_q2_is_convergent_&_lim_q2_in_rng_f_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= rng f implies ex q2 being Element of bool [:NAT,REAL:] st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) )
assume A3: rng s1 c= rng f ; ::_thesis: ex q2 being Element of bool [:NAT,REAL:] st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
defpred S1[ set , set ] means ( $2 in dom f & f . $2 = s1 . $1 );
A4: for n being Element of NAT ex p being Real st S1[n,p]
proof
let n be Element of NAT ; ::_thesis: ex p being Real st S1[n,p]
 s1 . n in rng s1 by VALUED_0:28;
then consider p being Element of REAL  such that
A5: ( p in dom f & s1 . n = f . p ) by A3, PARTFUN1:3;
take  p ; ::_thesis: S1[n,p]
thus  S1[n,p] by A5; ::_thesis: verum
end;
consider q1 being Real_Sequence such that
A6: for n being Element of NAT holds S1[n,q1 . n] from FUNCT_2:sch_3(A4);
now__::_thesis:_for_x_being_set_st_x_in_rng_q1_holds_
x_in_dom_f
let x be set ; ::_thesis: ( x in rng q1 implies x in dom f )
assume  x in rng q1 ; ::_thesis: x in dom f
then  ex n being Element of NAT st x = q1 . n by FUNCT_2:113;
hence  x in dom f by A6; ::_thesis: verum
end;
then A7: rng q1 c= dom f by TARSKI:def_3;
then consider s2 being Real_Sequence such that
A8: s2 is subsequence of q1 and
A9: s2 is convergent and
A10: lim s2 in dom f by A1, RCOMP_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(f_/*_q1)_._n_=_s1_._n
let n be Element of NAT ; ::_thesis: (f /* q1) . n = s1 . n
 f . (q1 . n) = s1 . n by A6;
hence  (f /* q1) . n = s1 . n by A7, FUNCT_2:108; ::_thesis: verum
end;
then A11: f /* q1 = s1 by FUNCT_2:63;
take q2 = f /* s2; ::_thesis: ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
 lim s2 in dom (f | (dom f)) by A10;
then  f | (dom f) is_continuous_in lim s2 by A2, Def2;
then A12: f is_continuous_in lim s2 ;
 rng s2 c= rng q1 by A8, VALUED_0:21;
then A13: rng s2 c= dom f by A7, XBOOLE_1:1;
then  f . (lim s2) = lim (f /* s2) by A9, A12, Def1;
hence  ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) by A7, A11, A8, A9, A10, A12, A13, Def1, FUNCT_1:def_3, VALUED_0:22; ::_thesis: verum
end;
hence  rng f is compact by RCOMP_1:def_3; ::_thesis: verum
end;

theorem :: FCONT_1:29
for Y being Subset of REAL
for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & f | Y is continuous holds
f .: Y is compact
proof
let Y be Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & f | Y is continuous holds
f .: Y is compact
let f be PartFunc of REAL,REAL; ::_thesis: ( Y c= dom f & Y is compact & f | Y is continuous implies f .: Y is compact )
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f | Y is continuous ; ::_thesis: f .: Y is compact
A4: (f | Y) | Y is continuous by A3;
dom (f | Y) = (dom f) /\ Y by RELAT_1:61
.= Y by A1, XBOOLE_1:28 ;
then  rng (f | Y) is compact by A2, A4, Th28;
hence  f .: Y is compact by RELAT_1:115; ::_thesis: verum
end;

theorem Th30: :: FCONT_1:30
for f being PartFunc of REAL,REAL st dom f <> {} & dom f is compact & f | (dom f) is continuous holds
ex x1, x2 being real number st
( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) )
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( dom f <> {} & dom f is compact & f | (dom f) is continuous implies ex x1, x2 being real number st
( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) ) )
assume  ( dom f <> {} & dom f is compact & f | (dom f) is continuous ) ; ::_thesis: ex x1, x2 being real number st
( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) )
then A1: ( rng f <> {} & rng f is compact ) by Th28, RELAT_1:42;
then consider x being Element of REAL  such that
A2: ( x in dom f & upper_bound (rng f) = f . x ) by PARTFUN1:3, RCOMP_1:14;
take  x ; ::_thesis: ex x2 being real number st
( x in dom f & x2 in dom f & f . x = upper_bound (rng f) & f . x2 = lower_bound (rng f) )
consider y being Element of REAL  such that
A3: ( y in dom f & lower_bound (rng f) = f . y ) by A1, PARTFUN1:3, RCOMP_1:14;
take  y ; ::_thesis: ( x in dom f & y in dom f & f . x = upper_bound (rng f) & f . y = lower_bound (rng f) )
thus  ( x in dom f & y in dom f & f . x = upper_bound (rng f) & f . y = lower_bound (rng f) ) by A2, A3; ::_thesis: verum
end;

theorem :: FCONT_1:31
for f being PartFunc of REAL,REAL
for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is continuous holds
ex x1, x2 being real number st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
proof
let f be PartFunc of REAL,REAL; ::_thesis: for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is continuous holds
ex x1, x2 being real number st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
let Y be Subset of REAL; ::_thesis: ( Y <> {} & Y c= dom f & Y is compact & f | Y is continuous implies ex x1, x2 being real number st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) )
assume that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f | Y is continuous ; ::_thesis: ex x1, x2 being real number st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
A5: dom (f | Y) = (dom f) /\ Y by RELAT_1:61
.= Y by A2, XBOOLE_1:28 ;
 (f | Y) | Y is continuous by A4;
then consider x1, x2 being real number  such that
A6: ( x1 in dom (f | Y) & x2 in dom (f | Y) ) and
A7: ( (f | Y) . x1 = upper_bound (rng (f | Y)) & (f | Y) . x2 = lower_bound (rng (f | Y)) ) by A1, A3, A5, Th30;
take  x1 ; ::_thesis: ex x2 being real number st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
take  x2 ; ::_thesis: ( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
thus  ( x1 in Y & x2 in Y ) by A6; ::_thesis: ( f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
 ( f . x1 = upper_bound (rng (f | Y)) & f . x2 = lower_bound (rng (f | Y)) ) by A6, A7, FUNCT_1:47;
hence  ( f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) by RELAT_1:115; ::_thesis: verum
end;

definition
let f be PartFunc of REAL,REAL;
attrf is Lipschitzian  means :Def3: :: FCONT_1:def 3
 ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) );
end;

:: deftheorem Def3 defines Lipschitzian FCONT_1:def_3_:_
 for f being PartFunc of REAL,REAL holds
( f is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) );

theorem Th32: :: FCONT_1:32
for X being set
for f being PartFunc of REAL,REAL holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) )
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) )
thus  ( f | X is Lipschitzian implies ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) ) ::_thesis: ( ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) implies f | X is Lipschitzian )
proof
given r being real number  such that A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2)) ; :: according to FCONT_1:def_3 ::_thesis: ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) )
take  r ; ::_thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) )
thus  0 < r by A1; ::_thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) )
assume A3: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2))
then  ( (f | X) . x1 = f . x1 & (f | X) . x2 = f . x2 ) by FUNCT_1:47;
hence  abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by A2, A3; ::_thesis: verum
end;
given r being real number  such that A4: 0 < r and
A5: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ; ::_thesis: f | X is Lipschitzian
take  r ; :: according to FCONT_1:def_3 ::_thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2)) ) )
thus  0 < r by A4; ::_thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2)) )
assume A6: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2))
then  ( (f | X) . x1 = f . x1 & (f | X) . x2 = f . x2 ) by FUNCT_1:47;
hence  abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2)) by A5, A6; ::_thesis: verum
end;

registration
cluster Function-like empty  ->  Lipschitzian for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st b1 is empty holds
b1 is Lipschitzian
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( f is empty implies f is Lipschitzian )
assume A1: f is empty ; ::_thesis: f is Lipschitzian
take  1 ; :: according to FCONT_1:def_3 ::_thesis: ( 0 < 1 & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) ) )
thus  ( 0 < 1 & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) ) ) by A1; ::_thesis: verum
end;
end;

registration
cluster Relation-like REAL -defined REAL -valued Function-like empty complex-valued ext-real-valued real-valued for Element of bool [:REAL,REAL:];
existence
 ex b1 being PartFunc of REAL,REAL st b1 is empty
proof
take  the empty PartFunc of REAL,REAL ; ::_thesis: the empty PartFunc of REAL,REAL is empty
thus  the empty PartFunc of REAL,REAL is empty ; ::_thesis: verum
end;
end;

registration
let f be Lipschitzian PartFunc of REAL,REAL;
let X be set ;
clusterf | X ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is Lipschitzian
proof
consider r being real number  such that
A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by Def3;
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_(f_|_X)_&_x2_in_dom_(f_|_X)_holds_
abs_((f_._x1)_-_(f_._x2))_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) )
assume  ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2))
then  ( x1 in dom f & x2 in dom f ) by RELAT_1:57;
hence  abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by A2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is Lipschitzian by A1, Th32; ::_thesis: verum
end;
end;

theorem :: FCONT_1:33
for X, X1 being set
for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
proof
let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is Lipschitzian & X1 c= X implies f | X1 is Lipschitzian )
assume that
A1: f | X is Lipschitzian and
A2: X1 c= X ; ::_thesis: f | X1 is Lipschitzian
 f | X1 = (f | X) | X1 by A2, RELAT_1:74;
hence  f | X1 is Lipschitzian by A1; ::_thesis: verum
end;

registration
let f1, f2 be Lipschitzian PartFunc of REAL,REAL;
clusterf1 + f2 ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f1 + f2 holds
b1 is Lipschitzian
proof
set X = dom f1;
set X1 = dom f2;
consider s being real number  such that
A1: 0 < s and
A2: for x1, x2 being real number st x1 in dom (f1 | ((dom f1) /\ (dom f2))) & x2 in dom (f1 | ((dom f1) /\ (dom f2))) holds
abs ((f1 . x1) - (f1 . x2)) <= s * (abs (x1 - x2)) by Th32;
consider g being real number  such that
A3: 0 < g and
A4: for x1, x2 being real number st x1 in dom (f2 | ((dom f1) /\ (dom f2))) & x2 in dom (f2 | ((dom f1) /\ (dom f2))) holds
abs ((f2 . x1) - (f2 . x2)) <= g * (abs (x1 - x2)) by Th32;
now__::_thesis:_ex_p_being_set_st_
(_0_<_p_&_(_for_x1,_x2_being_real_number_st_x1_in_dom_(f1_+_f2)_&_x2_in_dom_(f1_+_f2)_holds_
abs_(((f1_+_f2)_._x1)_-_((f1_+_f2)_._x2))_<=_p_*_(abs_(x1_-_x2))_)_)
take p = s + g; ::_thesis: ( 0 < p & ( for x1, x2 being real number st x1 in dom (f1 + f2) & x2 in dom (f1 + f2) holds
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2)) ) )
thus  0 < p by A1, A3; ::_thesis: for x1, x2 being real number st x1 in dom (f1 + f2) & x2 in dom (f1 + f2) holds
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f1 + f2) & x2 in dom (f1 + f2) implies abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2)) )
assume that
A5: x1 in dom (f1 + f2) and
A6: x2 in dom (f1 + f2) ; ::_thesis: abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2))
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) = abs (((f1 . x1) + (f2 . x1)) - ((f1 + f2) . x2)) by A5, VALUED_1:def_1
.= abs (((f1 . x1) + (f2 . x1)) - ((f1 . x2) + (f2 . x2))) by A6, VALUED_1:def_1
.= abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) ;
then A7: abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) by COMPLEX1:56;
dom (f2 | ((dom f1) /\ (dom f2))) = (dom f2) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f2) /\ (dom f2)) /\ (dom f1) by XBOOLE_1:16
.= dom (f1 + f2) by VALUED_1:def_1 ;
then A8: abs ((f2 . x1) - (f2 . x2)) <= g * (abs (x1 - x2)) by A4, A5, A6;
dom (f1 | ((dom f1) /\ (dom f2))) = (dom f1) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f1) /\ (dom f1)) /\ (dom f2) by XBOOLE_1:16
.= dom (f1 + f2) by VALUED_1:def_1 ;
then  abs ((f1 . x1) - (f1 . x2)) <= s * (abs (x1 - x2)) by A2, A5, A6;
then  (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) <= (s * (abs (x1 - x2))) + (g * (abs (x1 - x2))) by A8, XREAL_1:7;
hence  abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2)) by A7, XXREAL_0:2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = f1 + f2 holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
clusterf1 - f2 ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f1 - f2 holds
b1 is Lipschitzian
proof
set X = dom f1;
set X1 = dom f2;
consider s being real number  such that
A9: 0 < s and
A10: for x1, x2 being real number st x1 in dom (f1 | ((dom f1) /\ (dom f2))) & x2 in dom (f1 | ((dom f1) /\ (dom f2))) holds
abs ((f1 . x1) - (f1 . x2)) <= s * (abs (x1 - x2)) by Th32;
consider g being real number  such that
A11: 0 < g and
A12: for x1, x2 being real number st x1 in dom (f2 | ((dom f1) /\ (dom f2))) & x2 in dom (f2 | ((dom f1) /\ (dom f2))) holds
abs ((f2 . x1) - (f2 . x2)) <= g * (abs (x1 - x2)) by Th32;
now__::_thesis:_ex_p_being_set_st_
(_0_<_p_&_(_for_x1,_x2_being_real_number_st_x1_in_dom_(f1_-_f2)_&_x2_in_dom_(f1_-_f2)_holds_
abs_(((f1_-_f2)_._x1)_-_((f1_-_f2)_._x2))_<=_p_*_(abs_(x1_-_x2))_)_)
take p = s + g; ::_thesis: ( 0 < p & ( for x1, x2 being real number st x1 in dom (f1 - f2) & x2 in dom (f1 - f2) holds
abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) <= p * (abs (x1 - x2)) ) )
thus  0 < p by A9, A11; ::_thesis: for x1, x2 being real number st x1 in dom (f1 - f2) & x2 in dom (f1 - f2) holds
abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) <= p * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f1 - f2) & x2 in dom (f1 - f2) implies abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) <= p * (abs (x1 - x2)) )
assume that
A13: x1 in dom (f1 - f2) and
A14: x2 in dom (f1 - f2) ; ::_thesis: abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) <= p * (abs (x1 - x2))
abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) = abs (((f1 . x1) - (f2 . x1)) - ((f1 - f2) . x2)) by A13, VALUED_1:13
.= abs (((f1 . x1) - (f2 . x1)) - ((f1 . x2) - (f2 . x2))) by A14, VALUED_1:13
.= abs (((f1 . x1) - (f1 . x2)) - ((f2 . x1) - (f2 . x2))) ;
then A15: abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) <= (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) by COMPLEX1:57;
dom (f2 | ((dom f1) /\ (dom f2))) = (dom f2) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f2) /\ (dom f2)) /\ (dom f1) by XBOOLE_1:16
.= dom (f1 - f2) by VALUED_1:12 ;
then A16: abs ((f2 . x1) - (f2 . x2)) <= g * (abs (x1 - x2)) by A12, A13, A14;
dom (f1 | ((dom f1) /\ (dom f2))) = (dom f1) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f1) /\ (dom f1)) /\ (dom f2) by XBOOLE_1:16
.= dom (f1 - f2) by VALUED_1:12 ;
then  abs ((f1 . x1) - (f1 . x2)) <= s * (abs (x1 - x2)) by A10, A13, A14;
then  (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) <= (s * (abs (x1 - x2))) + (g * (abs (x1 - x2))) by A16, XREAL_1:7;
hence  abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) <= p * (abs (x1 - x2)) by A15, XXREAL_0:2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = f1 - f2 holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
end;

theorem :: FCONT_1:34
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
proof
let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 + f2) | (X /\ X1) is Lipschitzian )
A1: ( f1 | (X /\ X1) = (f1 | X) | (X /\ X1) & f2 | (X /\ X1) = (f2 | X1) | (X /\ X1) ) by RELAT_1:74, XBOOLE_1:17;
A2: (f1 + f2) | (X /\ X1) = (f1 | (X /\ X1)) + (f2 | (X /\ X1)) by RFUNCT_1:44;
assume  ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 + f2) | (X /\ X1) is Lipschitzian
hence  (f1 + f2) | (X /\ X1) is Lipschitzian by A1, A2; ::_thesis: verum
end;

theorem :: FCONT_1:35
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian
proof
let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 - f2) | (X /\ X1) is Lipschitzian )
A1: ( f1 | (X /\ X1) = (f1 | X) | (X /\ X1) & f2 | (X /\ X1) = (f2 | X1) | (X /\ X1) ) by RELAT_1:74, XBOOLE_1:17;
A2: (f1 - f2) | (X /\ X1) = (f1 | (X /\ X1)) - (f2 | (X /\ X1)) by RFUNCT_1:47;
assume  ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 - f2) | (X /\ X1) is Lipschitzian
hence  (f1 - f2) | (X /\ X1) is Lipschitzian by A1, A2; ::_thesis: verum
end;

registration
let f1, f2 be bounded Lipschitzian PartFunc of REAL,REAL;
clusterf1 (#) f2 ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = f1 (#) f2 holds
b1 is Lipschitzian
proof
set X = dom f1;
set X1 = dom f2;
consider x1 being real number  such that
A1: for r being set st r in dom f1 holds
abs (f1 . r) <= x1 by RFUNCT_1:72;
consider x2 being real number  such that
A2: for r being set st r in dom f2 holds
abs (f2 . r) <= x2 by RFUNCT_1:72;
consider g being real number  such that
A3: 0 < g and
A4: for x1, x2 being real number st x1 in dom f2 & x2 in dom f2 holds
abs ((f2 . x1) - (f2 . x2)) <= g * (abs (x1 - x2)) by Def3;
consider s being real number  such that
A5: 0 < s and
A6: for x1, x2 being real number st x1 in dom f1 & x2 in dom f1 holds
abs ((f1 . x1) - (f1 . x2)) <= s * (abs (x1 - x2)) by Def3;
A7: now__::_thesis:_for_r_being_real_number_st_r_in_dom_(f1_(#)_f2)_holds_
(_abs_(f1_._r)_<=_abs_x1_&_abs_(f2_._r)_<=_abs_x2_)
let r be real number ; ::_thesis: ( r in dom (f1 (#) f2) implies ( abs (f1 . r) <= abs x1 & abs (f2 . r) <= abs x2 ) )
assume  r in dom (f1 (#) f2) ; ::_thesis: ( abs (f1 . r) <= abs x1 & abs (f2 . r) <= abs x2 )
then A8: r in (dom f1) /\ (dom f2) by VALUED_1:def_4;
then  r in dom f1 by XBOOLE_0:def_4;
then A9: abs (f1 . r) <= x1 by A1;
 r in dom f2 by A8, XBOOLE_0:def_4;
then A10: abs (f2 . r) <= x2 by A2;
 x1 <= abs x1 by ABSVALUE:4;
hence  abs (f1 . r) <= abs x1 by A9, XXREAL_0:2; ::_thesis: abs (f2 . r) <= abs x2
 x2 <= abs x2 by ABSVALUE:4;
hence  abs (f2 . r) <= abs x2 by A10, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_ex_p_being_Element_of_REAL_st_
(_0_<_p_&_(_for_y1,_y2_being_real_number_st_y1_in_dom_(f1_(#)_f2)_&_y2_in_dom_(f1_(#)_f2)_holds_
abs_(((f1_(#)_f2)_._y1)_-_((f1_(#)_f2)_._y2))_<=_p_*_(abs_(y1_-_y2))_)_)
take p = (((abs x1) * g) + ((abs x2) * s)) + 1; ::_thesis: ( 0 < p & ( for y1, y2 being real number st y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) holds
abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2)) ) )
A11: 0 <= abs x1 by COMPLEX1:46;
 ( 0 <= abs x1 & 0 <= abs x2 ) by COMPLEX1:46;
hence  0 < p by A5, A3; ::_thesis: for y1, y2 being real number st y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) holds
abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2))
let y1, y2 be real number ; ::_thesis: ( y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) implies abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2)) )
assume that
A12: y1 in dom (f1 (#) f2) and
A13: y2 in dom (f1 (#) f2) ; ::_thesis: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2))
A14: y2 in (dom f1) /\ (dom f2) by A13, VALUED_1:def_4;
then A15: y2 in dom f1 by XBOOLE_0:def_4;
 ( abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) = (abs (f1 . y1)) * (abs ((f2 . y1) - (f2 . y2))) & 0 <= abs ((f2 . y1) - (f2 . y2)) ) by COMPLEX1:46, COMPLEX1:65;
then A16: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) <= (abs x1) * (abs ((f2 . y1) - (f2 . y2))) by A7, A12, XREAL_1:64;
A17: y2 in dom f2 by A14, XBOOLE_0:def_4;
A18: y1 in (dom f1) /\ (dom f2) by A12, VALUED_1:def_4;
then  y1 in dom f2 by XBOOLE_0:def_4;
then  (abs x1) * (abs ((f2 . y1) - (f2 . y2))) <= (abs x1) * (g * (abs (y1 - y2))) by A4, A17, A11, XREAL_1:64;
then A19: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) <= ((abs x1) * g) * (abs (y1 - y2)) by A16, XXREAL_0:2;
 0 <= abs (y1 - y2) by COMPLEX1:46;
then A20: ((((abs x1) * g) + ((abs x2) * s)) * (abs (y1 - y2))) + 0 <= ((((abs x1) * g) + ((abs x2) * s)) * (abs (y1 - y2))) + (1 * (abs (y1 - y2))) by XREAL_1:7;
abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) = abs (((f1 . y1) * (f2 . y1)) - ((f1 (#) f2) . y2)) by VALUED_1:5
.= abs ((((f1 . y1) * (f2 . y1)) + (((f1 . y1) * (f2 . y2)) - ((f1 . y1) * (f2 . y2)))) - ((f1 . y2) * (f2 . y2))) by VALUED_1:5
.= abs (((f1 . y1) * ((f2 . y1) - (f2 . y2))) + (((f1 . y1) - (f1 . y2)) * (f2 . y2))) ;
then A21: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) by COMPLEX1:56;
 ( abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) = (abs (f2 . y2)) * (abs ((f1 . y1) - (f1 . y2))) & 0 <= abs ((f1 . y1) - (f1 . y2)) ) by COMPLEX1:46, COMPLEX1:65;
then A22: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) <= (abs x2) * (abs ((f1 . y1) - (f1 . y2))) by A7, A13, XREAL_1:64;
A23: 0 <= abs x2 by COMPLEX1:46;
 y1 in dom f1 by A18, XBOOLE_0:def_4;
then  (abs x2) * (abs ((f1 . y1) - (f1 . y2))) <= (abs x2) * (s * (abs (y1 - y2))) by A6, A15, A23, XREAL_1:64;
then  abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) <= (abs x2) * (s * (abs (y1 - y2))) by A22, XXREAL_0:2;
then  (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) <= (((abs x1) * g) * (abs (y1 - y2))) + (((abs x2) * s) * (abs (y1 - y2))) by A19, XREAL_1:7;
then  abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= (((abs x1) * g) + ((abs x2) * s)) * (abs (y1 - y2)) by A21, XXREAL_0:2;
hence  abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2)) by A20, XXREAL_0:2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = f1 (#) f2 holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
end;

theorem :: FCONT_1:36
for X, X1, Z, Z1 being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded holds
(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian
proof
let X, X1, Z, Z1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded holds
(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded implies (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian )
A1: f1 | (((X /\ Z) /\ X1) /\ Z1) = f1 | ((X1 /\ Z1) /\ (X /\ Z)) by XBOOLE_1:16
.= f1 | (((X1 /\ Z1) /\ X) /\ Z) by XBOOLE_1:16
.= (f1 | Z) | ((X1 /\ Z1) /\ X) by RELAT_1:71 ;
A2: f1 | (((X /\ Z) /\ X1) /\ Z1) = f1 | ((X1 /\ Z1) /\ (X /\ Z)) by XBOOLE_1:16
.= f1 | (((X1 /\ Z1) /\ Z) /\ X) by XBOOLE_1:16
.= (f1 | X) | ((X1 /\ Z1) /\ Z) by RELAT_1:71 ;
A3: f2 | (((X /\ Z) /\ X1) /\ Z1) = f2 | (((X /\ Z) /\ Z1) /\ X1) by XBOOLE_1:16
.= (f2 | X1) | ((Z /\ X) /\ Z1) by RELAT_1:71 ;
A4: ( (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) = (f1 | (((X /\ Z) /\ X1) /\ Z1)) (#) (f2 | (((X /\ Z) /\ X1) /\ Z1)) & f2 | (((X /\ Z) /\ X1) /\ Z1) = (f2 | Z1) | ((X /\ Z) /\ X1) ) by RELAT_1:71, RFUNCT_1:45;
assume  ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded ) ; ::_thesis: (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian
hence  (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian by A1, A2, A4, A3; ::_thesis: verum
end;

registration
let f be Lipschitzian PartFunc of REAL,REAL;
let p be real number ;
clusterp (#) f ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = p (#) f holds
b1 is Lipschitzian
proof
consider s being real number  such that
A1: 0 < s and
A2: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= s * (abs (x1 - x2)) by Def3;
percases ( p = 0 or p <> 0 ) ;
supposeA3: p = 0 ; ::_thesis: for b1 being PartFunc of REAL,REAL st b1 = p (#) f holds
b1 is Lipschitzian
now__::_thesis:_ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1,_x2_being_real_number_st_x1_in_dom_(p_(#)_f)_&_x2_in_dom_(p_(#)_f)_holds_
abs_(((p_(#)_f)_._x1)_-_((p_(#)_f)_._x2))_<=_s_*_(abs_(x1_-_x2))_)_)
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2)) ) )
thus  0 < s by A1; ::_thesis: for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) implies abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2)) )
assume that
A4: x1 in dom (p (#) f) and
A5: x2 in dom (p (#) f) ; ::_thesis: abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2))
A6: 0 <= abs (x1 - x2) by COMPLEX1:46;
abs (((p (#) f) . x1) - ((p (#) f) . x2)) = abs ((p * (f . x1)) - ((p (#) f) . x2)) by A4, VALUED_1:def_5
.= abs (0 - (p * (f . x2))) by A3, A5, VALUED_1:def_5
.= 0 by A3, ABSVALUE:2 ;
hence  abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2)) by A1, A6; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = p (#) f holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
suppose p <> 0 ; ::_thesis: for b1 being PartFunc of REAL,REAL st b1 = p (#) f holds
b1 is Lipschitzian
then  0 < abs p by COMPLEX1:47;
then A7: 0 * s < (abs p) * s by A1, XREAL_1:68;
now__::_thesis:_ex_g_being_Element_of_REAL_st_
(_0_<_g_&_(_for_x1,_x2_being_real_number_st_x1_in_dom_(p_(#)_f)_&_x2_in_dom_(p_(#)_f)_holds_
abs_(((p_(#)_f)_._x1)_-_((p_(#)_f)_._x2))_<=_g_*_(abs_(x1_-_x2))_)_)
take g = (abs p) * s; ::_thesis: ( 0 < g & ( for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2)) ) )
A8: 0 <= abs p by COMPLEX1:46;
thus  0 < g by A7; ::_thesis: for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) implies abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2)) )
assume that
A9: x1 in dom (p (#) f) and
A10: x2 in dom (p (#) f) ; ::_thesis: abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2))
A11: abs (((p (#) f) . x1) - ((p (#) f) . x2)) = abs ((p * (f . x1)) - ((p (#) f) . x2)) by A9, VALUED_1:def_5
.= abs ((p * (f . x1)) - (p * (f . x2))) by A10, VALUED_1:def_5
.= abs (p * ((f . x1) - (f . x2)))
.= (abs p) * (abs ((f . x1) - (f . x2))) by COMPLEX1:65 ;
 ( x1 in dom f & x2 in dom f ) by A9, A10, VALUED_1:def_5;
then  (abs p) * (abs ((f . x1) - (f . x2))) <= (abs p) * (s * (abs (x1 - x2))) by A2, A8, XREAL_1:64;
hence  abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2)) by A11; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = p (#) f holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
end;
end;
end;

theorem :: FCONT_1:37
for X being set
for p being real number
for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
proof
let X be set ; ::_thesis: for p being real number
for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
let p be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian )
 (p (#) f) | X = p (#) (f | X) by RFUNCT_1:49;
hence  ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian ) ; ::_thesis: verum
end;

registration
let f be Lipschitzian PartFunc of REAL,REAL;
cluster|.f.| ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = abs f holds
b1 is Lipschitzian
proof
consider s being real number  such that
A1: 0 < s and
A2: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= s * (abs (x1 - x2)) by Def3;
now__::_thesis:_ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1,_x2_being_real_number_st_x1_in_dom_(abs_f)_&_x2_in_dom_(abs_f)_holds_
abs_(((abs_f)_._x1)_-_((abs_f)_._x2))_<=_s_*_(abs_(x1_-_x2))_)_)
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being real number st x1 in dom (abs f) & x2 in dom (abs f) holds
abs (((abs f) . x1) - ((abs f) . x2)) <= s * (abs (x1 - x2)) ) )
thus  0 < s by A1; ::_thesis: for x1, x2 being real number st x1 in dom (abs f) & x2 in dom (abs f) holds
abs (((abs f) . x1) - ((abs f) . x2)) <= s * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (abs f) & x2 in dom (abs f) implies abs (((abs f) . x1) - ((abs f) . x2)) <= s * (abs (x1 - x2)) )
assume  ( x1 in dom (abs f) & x2 in dom (abs f) ) ; ::_thesis: abs (((abs f) . x1) - ((abs f) . x2)) <= s * (abs (x1 - x2))
then  ( x1 in dom f & x2 in dom f ) by VALUED_1:def_11;
then A3: abs ((f . x1) - (f . x2)) <= s * (abs (x1 - x2)) by A2;
abs (((abs f) . x1) - ((abs f) . x2)) = abs ((abs (f . x1)) - ((abs f) . x2)) by VALUED_1:18
.= abs ((abs (f . x1)) - (abs (f . x2))) by VALUED_1:18 ;
then  abs (((abs f) . x1) - ((abs f) . x2)) <= abs ((f . x1) - (f . x2)) by COMPLEX1:64;
hence  abs (((abs f) . x1) - ((abs f) . x2)) <= s * (abs (x1 - x2)) by A3, XXREAL_0:2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = abs f holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
end;

theorem :: FCONT_1:38
for X being set
for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is Lipschitzian implies ( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian ) )
assume A1: f | X is Lipschitzian ; ::_thesis: ( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )
hence  - (f | X) is Lipschitzian ; ::_thesis: (abs f) | X is Lipschitzian
 (abs f) | X = abs (f | X) by RFUNCT_1:46;
hence  (abs f) | X is Lipschitzian by A1; ::_thesis: verum
end;

registration
cluster Function-like V8()  ->  Lipschitzian for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st b1 is V8() holds
b1 is Lipschitzian
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( f is V8() implies f is Lipschitzian )
assume A1: f is V8() ; ::_thesis: f is Lipschitzian
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_f_&_x2_in_dom_f_holds_
abs_((f_._x1)_-_(f_._x2))_<=_1_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) )
assume  ( x1 in dom f & x2 in dom f ) ; ::_thesis: abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2))
then  f . x1 = f . x2 by A1, FUNCT_1:def_10;
then  abs ((f . x1) - (f . x2)) = 0 by ABSVALUE:2;
hence  abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) by COMPLEX1:46; ::_thesis: verum
end;
hence  f is Lipschitzian by Def3; ::_thesis: verum
end;
end;

registration
let Y be Subset of REAL;
cluster id Y ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = id Y holds
b1 is Lipschitzian
proof
reconsider r = 1 as Real ;
 id Y is Lipschitzian
proof
take  r ; :: according to FCONT_1:def_3 ::_thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (id Y) & x2 in dom (id Y) holds
abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2)) ) )
thus  r > 0 ; ::_thesis: for x1, x2 being real number st x1 in dom (id Y) & x2 in dom (id Y) holds
abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (id Y) & x2 in dom (id Y) implies abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2)) )
assume that
A1: x1 in dom (id Y) and
A2: x2 in dom (id Y) ; ::_thesis: abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2))
A3: x2 in Y by A2;
 x1 in Y by A1;
then  abs (((id Y) . x1) - ((id Y) . x2)) = abs (x1 - ((id Y) . x2)) by FUNCT_1:18
.= r * (abs (x1 - x2)) by A3, FUNCT_1:18 ;
hence  abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2)) ; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = id Y holds
b1 is Lipschitzian ; ::_thesis: verum
end;
end;

registration
cluster Function-like Lipschitzian  ->  continuous for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st b1 is Lipschitzian holds
b1 is continuous
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( f is Lipschitzian implies f is continuous )
set X = dom f;
assume  f is Lipschitzian ; ::_thesis: f is continuous
then consider r being real number  such that
A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by Def3;
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_f_holds_
f_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom f implies f is_continuous_in x0 )
assume A3: x0 in dom f ; ::_thesis: f is_continuous_in x0
 for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < r ) )
proof
let g be real number ; ::_thesis: ( 0 < g implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < g ) ) )
assume A4: 0 < g ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
abs ((f . x1) - (f . x0)) < g ) )
set s = g / r;
take s9 = g / r; ::_thesis: ( 0 < s9 & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s9 holds
abs ((f . x1) - (f . x0)) < g ) )
A5: now__::_thesis:_for_x1_being_real_number_st_x1_in_dom_f_&_abs_(x1_-_x0)_<_g_/_r_holds_
abs_((f_._x1)_-_(f_._x0))_<_g
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < g / r implies abs ((f . x1) - (f . x0)) < g )
assume that
A6: x1 in dom f and
A7: abs (x1 - x0) < g / r ; ::_thesis: abs ((f . x1) - (f . x0)) < g
 r * (abs (x1 - x0)) < (g / r) * r by A1, A7, XREAL_1:68;
then A8: r * (abs (x1 - x0)) < g by A1, XCMPLX_1:87;
 abs ((f . x1) - (f . x0)) <= r * (abs (x1 - x0)) by A2, A3, A6;
hence  abs ((f . x1) - (f . x0)) < g by A8, XXREAL_0:2; ::_thesis: verum
end;
 s9 = g * (r ") by XCMPLX_0:def_9;
hence  ( 0 < s9 & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s9 holds
abs ((f . x1) - (f . x0)) < g ) ) by A1, A4, A5, XREAL_1:129; ::_thesis: verum
end;
hence  f is_continuous_in x0 by Th3; ::_thesis: verum
end;
hence  f is continuous by Def2; ::_thesis: verum
end;
end;

theorem :: FCONT_1:39
for f being PartFunc of REAL,REAL st ex r being real number st rng f = {r} holds
f is continuous
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( ex r being real number st rng f = {r} implies f is continuous )
given r being real number  such that A1: rng f = {r} ; ::_thesis: f is continuous
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_f_&_x2_in_dom_f_holds_
abs_((f_._x1)_-_(f_._x2))_<=_1_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) )
assume that
A2: x1 in dom f and
A3: x2 in dom f ; ::_thesis: abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2))
 f . x2 in rng f by A3, FUNCT_1:def_3;
then A4: f . x2 = r by A1, TARSKI:def_1;
 f . x1 in rng f by A2, FUNCT_1:def_3;
then  f . x1 = r by A1, TARSKI:def_1;
then  abs ((f . x1) - (f . x2)) = 0 by A4, ABSVALUE:2;
hence  abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) by COMPLEX1:46; ::_thesis: verum
end;
then  f is Lipschitzian by Def3;
hence  f is continuous ; ::_thesis: verum
end;

theorem :: FCONT_1:40
for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in dom f holds
f . x0 = x0 ) holds
f is continuous
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( ( for x0 being real number st x0 in dom f holds
f . x0 = x0 ) implies f is continuous )
assume A1: for x0 being real number st x0 in dom f holds
f . x0 = x0 ; ::_thesis: f is continuous
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_f_&_x2_in_dom_f_holds_
abs_((f_._x1)_-_(f_._x2))_<=_1_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) )
assume that
A2: x1 in dom f and
A3: x2 in dom f ; ::_thesis: abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2))
 f . x1 = x1 by A1, A2;
hence  abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) by A1, A3; ::_thesis: verum
end;
then  f is Lipschitzian by Def3;
hence  f is continuous ; ::_thesis: verum
end;

theorem Th41: :: FCONT_1:41
for X being set
for r, p being real number
for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ) holds
f | X is continuous
proof
let X be set ; ::_thesis: for r, p being real number
for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ) holds
f | X is continuous
let r, p be real number ; ::_thesis: for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ) holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( ( for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ) implies f | X is continuous )
assume A1: for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ; ::_thesis: f | X is continuous
A2: now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_(f_|_X)_&_x2_in_dom_(f_|_X)_holds_
abs_((f_._x1)_-_(f_._x2))_<=_((abs_r)_+_1)_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies abs ((f . x1) - (f . x2)) <= ((abs r) + 1) * (abs (x1 - x2)) )
assume that
A3: x1 in dom (f | X) and
A4: x2 in dom (f | X) ; ::_thesis: abs ((f . x1) - (f . x2)) <= ((abs r) + 1) * (abs (x1 - x2))
 x2 in X by A4;
then A5: f . x2 = (r * x2) + p by A1;
A6: 0 <= abs (x1 - x2) by COMPLEX1:46;
 x1 in X by A3;
then  f . x1 = (r * x1) + p by A1;
then  abs ((f . x1) - (f . x2)) = abs (r * (x1 - x2)) by A5
.= (abs r) * (abs (x1 - x2)) by COMPLEX1:65 ;
then  (abs ((f . x1) - (f . x2))) + 0 <= ((abs r) * (abs (x1 - x2))) + (1 * (abs (x1 - x2))) by A6, XREAL_1:7;
hence  abs ((f . x1) - (f . x2)) <= ((abs r) + 1) * (abs (x1 - x2)) ; ::_thesis: verum
end;
 0 + 0 < (abs r) + 1 by COMPLEX1:46, XREAL_1:8;
then  f | X is Lipschitzian by A2, Th32;
hence  f | X is continuous ; ::_thesis: verum
end;

theorem Th42: :: FCONT_1:42
for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in dom f holds
f . x0 = x0 ^2 ) holds
f | (dom f) is continuous
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( ( for x0 being real number st x0 in dom f holds
f . x0 = x0 ^2 ) implies f | (dom f) is continuous )
reconsider f1 = id (dom f) as PartFunc of REAL,REAL ;
assume A1: for x0 being real number st x0 in dom f holds
f . x0 = x0 ^2 ; ::_thesis: f | (dom f) is continuous
A2: now__::_thesis:_for_x0_being_set_st_x0_in_dom_f_holds_
f_._x0_=_(f1_._x0)_*_(f1_._x0)
let x0 be set ; ::_thesis: ( x0 in dom f implies f . x0 = (f1 . x0) * (f1 . x0) )
assume A3: x0 in dom f ; ::_thesis: f . x0 = (f1 . x0) * (f1 . x0)
then reconsider x1 = x0 as Real ;
thus f . x0 = x1 ^2 by A1, A3
.= (f1 . x1) * x1 by A3, FUNCT_1:18
.= (f1 . x0) * (f1 . x0) by A3, FUNCT_1:18 ; ::_thesis: verum
end;
 (dom f1) /\ (dom f1) = dom f by RELAT_1:45;
then  f = f1 (#) f1 by A2, VALUED_1:def_4;
hence  f | (dom f) is continuous ; ::_thesis: verum
end;

theorem :: FCONT_1:43
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & ( for x0 being real number st x0 in X holds
f . x0 = x0 ^2 ) holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & ( for x0 being real number st x0 in X holds
f . x0 = x0 ^2 ) holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & ( for x0 being real number st x0 in X holds
f . x0 = x0 ^2 ) implies f | X is continuous )
assume that
A1: X c= dom f and
A2: for x0 being real number st x0 in X holds
f . x0 = x0 ^2 ; ::_thesis: f | X is continuous
 X = (dom f) /\ X by A1, XBOOLE_1:28;
then A3: X = dom (f | X) by RELAT_1:61;
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_(f_|_X)_holds_
(f_|_X)_._x0_=_x0_^2
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies (f | X) . x0 = x0 ^2 )
assume A4: x0 in dom (f | X) ; ::_thesis: (f | X) . x0 = x0 ^2
then  f . x0 = x0 ^2 by A2;
hence  (f | X) . x0 = x0 ^2 by A4, FUNCT_1:47; ::_thesis: verum
end;
then  (f | X) | X is continuous by A3, Th42;
hence  f | X is continuous ; ::_thesis: verum
end;

theorem Th44: :: FCONT_1:44
for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in dom f holds
f . x0 = abs x0 ) holds
f is continuous
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( ( for x0 being real number st x0 in dom f holds
f . x0 = abs x0 ) implies f is continuous )
assume A1: for x0 being real number st x0 in dom f holds
f . x0 = abs x0 ; ::_thesis: f is continuous
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_f_&_x2_in_dom_f_holds_
abs_((f_._x1)_-_(f_._x2))_<=_1_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) )
assume  ( x1 in dom f & x2 in dom f ) ; ::_thesis: abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2))
then  ( f . x1 = abs x1 & f . x2 = abs x2 ) by A1;
hence  abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) by COMPLEX1:64; ::_thesis: verum
end;
then  f is Lipschitzian by Def3;
hence  f is continuous ; ::_thesis: verum
end;

theorem :: FCONT_1:45
for X being set
for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in X holds
f . x0 = abs x0 ) holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in X holds
f . x0 = abs x0 ) holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( ( for x0 being real number st x0 in X holds
f . x0 = abs x0 ) implies f | X is continuous )
assume A1: for x0 being real number st x0 in X holds
f . x0 = abs x0 ; ::_thesis: f | X is continuous
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_(f_|_X)_holds_
(f_|_X)_._x0_=_abs_x0
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies (f | X) . x0 = abs x0 )
assume A2: x0 in dom (f | X) ; ::_thesis: (f | X) . x0 = abs x0
then  f . x0 = abs x0 by A1;
hence  (f | X) . x0 = abs x0 by A2, FUNCT_1:47; ::_thesis: verum
end;
hence  f | X is continuous by Th44; ::_thesis: verum
end;

theorem Th46: :: FCONT_1:46
for X being set
for f being PartFunc of REAL,REAL st f | X is monotone & ex p, g being real number st
( p <= g & f .: X = [.p,g.] ) holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is monotone & ex p, g being real number st
( p <= g & f .: X = [.p,g.] ) holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is monotone & ex p, g being real number st
( p <= g & f .: X = [.p,g.] ) implies f | X is continuous )
assume A1: f | X is monotone ; ::_thesis: ( for p, g being real number holds
( not p <= g or not f .: X = [.p,g.] ) or f | X is continuous )
given p, g being real number  such that A2: p <= g and
A3: f .: X = [.p,g.] ; ::_thesis: f | X is continuous
reconsider p = p, g = g as Real by XREAL_0:def_1;
now__::_thesis:_f_|_X_is_continuous
percases ( p = g or p < g ) by A2, XXREAL_0:1;
suppose p = g ; ::_thesis: f | X is continuous
then  f .: X = {p} by A3, XXREAL_1:17;
then  rng (f | X) = {p} by RELAT_1:115;
then  f | X is V8() ;
hence  f | X is continuous ; ::_thesis: verum
end;
supposeA4: p < g ; ::_thesis: f | X is continuous
now__::_thesis:_f_|_X_is_continuous
percases ( f | X is non-decreasing or f | X is non-increasing ) by A1, RFUNCT_2:def_5;
suppose f | X is non-decreasing ; ::_thesis: f | X is continuous
then A5: (f | X) | X is non-decreasing ;
 for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
A6: [.p,g.] = ].p,g.[ \/ {p,g} by A2, XXREAL_1:128;
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A7: (f | X) .: X = f .: X by RELAT_1:129;
assume A8: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
A9: (f | X) . x0 in (f | X) .: X by A8, FUNCT_1:def_6;
reconsider x0 = x0 as Real by XREAL_0:def_1;
 (f | X) . x0 in [.p,g.] by A3, A9, RELAT_1:129;
then A10: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A6, XBOOLE_0:def_3;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x1_being_real_number_st_x1_in_dom_(f_|_X)_&_x1_in_N_holds_
(f_|_X)_._x1_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1
now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_Real_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
percases ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 = p or (f | X) . x0 = g ) by A10, TARSKI:def_2;
suppose (f | X) . x0 in ].p,g.[ ; ::_thesis: ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider N2 being Neighbourhood of (f | X) . x0 such that
A11: N2 c= ].p,g.[ by RCOMP_1:18;
A12: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider N3 being Neighbourhood of (f | X) . x0 such that
A13: N3 c= N1 and
A14: N3 c= N2 by RCOMP_1:17;
consider r being real number  such that
A15: r > 0 and
A16: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A17: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A18: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;
A19: (f | X) . x0 < ((f | X) . x0) + r by A15, XREAL_1:29;
then  ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then  ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A18, XXREAL_0:2;
then  ((f | X) . x0) + (r / 2) in  {  s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r )  }  by A17;
then A20: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_2;
then  ((f | X) . x0) + (r / 2) in N2 by A14, A16;
then  ((f | X) . x0) + (r / 2) in ].p,g.[ by A11;
then consider x2 being Real such that
A21: ( x2 in dom (f | X) & x2 in X ) and
A22: ((f | X) . x0) + (r / 2) = (f | X) . x2 by A3, A7, A12, PARTFUN2:59;
A23: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
set M1 = ((f | X) . x0) - (r / 2);
A24: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;
 ((f | X) . x0) - (r / 2) < (f | X) . x0 by A18, XREAL_1:19;
then  ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A19, XXREAL_0:2;
then  ((f | X) . x0) - (r / 2) in  {  s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r )  }  by A24;
then A25: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_2;
then  ((f | X) . x0) - (r / 2) in N2 by A14, A16;
then  ((f | X) . x0) - (r / 2) in ].p,g.[ by A11;
then consider x1 being Real such that
A26: ( x1 in dom (f | X) & x1 in X ) and
A27: ((f | X) . x0) - (r / 2) = (f | X) . x1 by A3, A7, A23, PARTFUN2:59;
A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A15, XREAL_1:29, XREAL_1:215;
then A29: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A30: now__::_thesis:_not_x0_<_x1
assume A31: x0 < x1 ; ::_thesis: contradiction
 ( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A26, XBOOLE_0:def_4;
hence  contradiction by A5, A27, A29, A31, RFUNCT_2:22; ::_thesis: verum
end;
A32: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A15, XREAL_1:29, XREAL_1:215;
A33: now__::_thesis:_not_x2_<_x0
assume A34: x2 < x0 ; ::_thesis: contradiction
 ( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by A8, A21, XBOOLE_0:def_4;
hence  contradiction by A5, A22, A32, A34, RFUNCT_2:22; ::_thesis: verum
end;
 x0 <> x2 by A15, A22, XREAL_1:29, XREAL_1:215;
then  x0 < x2 by A33, XXREAL_0:1;
then A35: x2 - x0 > 0 by XREAL_1:50;
set R = min ((x0 - x1),(x2 - x0));
A36: min ((x0 - x1),(x2 - x0)) <= x2 - x0 by XXREAL_0:17;
 x1 <> x0 by A27, A28, XREAL_1:19;
then  x1 < x0 by A30, XXREAL_0:1;
then  x0 - x1 > 0 by XREAL_1:50;
then  min ((x0 - x1),(x2 - x0)) > 0 by A35, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((x0 - x1),(x2 - x0)))),(x0 + (min ((x0 - x1),(x2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be Real; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A37: x in dom (f | X) and
A38: x in N ; ::_thesis: (f | X) . x in N1
A39: x in X /\ (dom (f | X)) by A37, XBOOLE_1:28;
 x in  {  s where s is Real : ( x0 - (min ((x0 - x1),(x2 - x0))) < s & s < x0 + (min ((x0 - x1),(x2 - x0))) )  }  by A38, RCOMP_1:def_2;
then A40: ex s being Real st
( s = x & x0 - (min ((x0 - x1),(x2 - x0))) < s & s < x0 + (min ((x0 - x1),(x2 - x0))) ) ;
then  x0 < (min ((x0 - x1),(x2 - x0))) + x by XREAL_1:19;
then A41: x0 - x < ((min ((x0 - x1),(x2 - x0))) + x) - x by XREAL_1:9;
 min ((x0 - x1),(x2 - x0)) <= x0 - x1 by XXREAL_0:17;
then  x0 - x < x0 - x1 by A41, XXREAL_0:2;
then  - (x0 - x) > - (x0 - x1) by XREAL_1:24;
then A42: (x - x0) + x0 > (x1 - x0) + x0 by XREAL_1:6;
 x1 in X /\ (dom (f | X)) by A26, XBOOLE_0:def_4;
then A43: (f | X) . x1 <= (f | X) . x by A5, A42, A39, RFUNCT_2:22;
 x - x0 < min ((x0 - x1),(x2 - x0)) by A40, XREAL_1:19;
then  x - x0 < x2 - x0 by A36, XXREAL_0:2;
then A44: (x - x0) + x0 < (x2 - x0) + x0 by XREAL_1:6;
 x2 in X /\ (dom (f | X)) by A21, XBOOLE_0:def_4;
then  (f | X) . x <= (f | X) . x2 by A5, A44, A39, RFUNCT_2:22;
then  (f | X) . x in  {  s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) )  }  by A27, A22, A43;
then A45: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by RCOMP_1:def_1;
 [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A25, A20, XXREAL_2:def_12;
then  (f | X) . x in N3 by A16, A45;
hence  (f | X) . x in N1 by A13; ::_thesis: verum
end;
supposeA46: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider r being real number  such that
A47: r > 0 and
A48: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
set R = (min (r,(g - p))) / 2;
 g - p > 0 by A4, XREAL_1:50;
then A49: min (r,(g - p)) > 0 by A47, XXREAL_0:15;
then A50: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
 min (r,(g - p)) <= r by XXREAL_0:17;
then A51: (min (r,(g - p))) / 2 < r by A50, XXREAL_0:2;
then A52: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;
A53: p - ((min (r,(g - p))) / 2) < p by A49, XREAL_1:44, XREAL_1:215;
 - r < - ((min (r,(g - p))) / 2) by A51, XREAL_1:24;
then A54: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
 p < p + r by A47, XREAL_1:29;
then  p - ((min (r,(g - p))) / 2) < p + r by A53, XXREAL_0:2;
then  p - ((min (r,(g - p))) / 2) in  {  s where s is Real : ( p - r < s & s < p + r )  }  by A54;
then A55: p - ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def_2;
A56: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
A57: p < p + ((min (r,(g - p))) / 2) by A49, XREAL_1:29, XREAL_1:215;
 min (r,(g - p)) <= g - p by XXREAL_0:17;
then  (min (r,(g - p))) / 2 < g - p by A50, XXREAL_0:2;
then  p + ((min (r,(g - p))) / 2) < g by XREAL_1:20;
then  p + ((min (r,(g - p))) / 2) in  {  s where s is Real : ( p < s & s < g )  }  by A57;
then  p + ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def_2;
then consider x1 being Real such that
A58: ( x1 in dom (f | X) & x1 in X ) and
A59: p + ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A7, A56, PARTFUN2:59;
A60: x1 in X /\ (dom (f | X)) by A58, XBOOLE_0:def_4;
now__::_thesis:_not_x1_<_x0
assume A61: x1 < x0 ; ::_thesis: contradiction
 ( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A58, XBOOLE_0:def_4;
hence  contradiction by A5, A46, A57, A59, A61, RFUNCT_2:22; ::_thesis: verum
end;
then  x0 < x1 by A46, A57, A59, XXREAL_0:1;
then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def_6, XREAL_1:50;
take N = N; ::_thesis: for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be Real; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A62: x in dom (f | X) and
A63: x in N ; ::_thesis: (f | X) . x in N1
 x in  {  s where s is Real : ( x0 - (x1 - x0) < s & s < x0 + (x1 - x0) )  }  by A63, RCOMP_1:def_2;
then A64: ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
 (f | X) . x in [.p,g.] by A3, A7, A62, FUNCT_1:def_6;
then  (f | X) . x in  {  s where s is Real : ( p <= s & s <= g )  }  by RCOMP_1:def_1;
then  ex s being Real st
( s = (f | X) . x & p <= s & s <= g ) ;
then A65: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A53, XXREAL_0:2;
 x in X /\ (dom (f | X)) by A62, XBOOLE_0:def_4;
then  (f | X) . x <= p + ((min (r,(g - p))) / 2) by A5, A59, A60, A64, RFUNCT_2:22;
then  (f | X) . x in  {  s where s is Real : ( p - ((min (r,(g - p))) / 2) <= s & s <= p + ((min (r,(g - p))) / 2) )  }  by A65;
then A66: (f | X) . x in [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] by RCOMP_1:def_1;
 p - r < p by A47, XREAL_1:44;
then  p - r < p + ((min (r,(g - p))) / 2) by A57, XXREAL_0:2;
then  p + ((min (r,(g - p))) / 2) in  {  s where s is Real : ( p - r < s & s < p + r )  }  by A52;
then  p + ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def_2;
then  [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] c= N1 by A48, A55, XXREAL_2:def_12;
hence  (f | X) . x in N1 by A66; ::_thesis: verum
end;
supposeA67: (f | X) . x0 = g ; ::_thesis: ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
A68: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider r being real number  such that
A69: r > 0 and
A70: N1 = ].(g - r),(g + r).[ by A67, RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
set R = (min (r,(g - p))) / 2;
 g - p > 0 by A4, XREAL_1:50;
then A71: min (r,(g - p)) > 0 by A69, XXREAL_0:15;
then A72: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
A73: g - ((min (r,(g - p))) / 2) < g by A71, XREAL_1:44, XREAL_1:215;
 min (r,(g - p)) <= g - p by XXREAL_0:17;
then  (min (r,(g - p))) / 2 < g - p by A72, XXREAL_0:2;
then  ((min (r,(g - p))) / 2) + p < g by XREAL_1:20;
then  g - ((min (r,(g - p))) / 2) > p by XREAL_1:20;
then  g - ((min (r,(g - p))) / 2) in  {  s where s is Real : ( p < s & s < g )  }  by A73;
then  g - ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def_2;
then consider x1 being Real such that
A74: ( x1 in dom (f | X) & x1 in X ) and
A75: g - ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A7, A68, PARTFUN2:59;
A76: now__::_thesis:_not_x0_<_x1
assume A77: x0 < x1 ; ::_thesis: contradiction
 ( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A8, A74, XBOOLE_0:def_4;
hence  contradiction by A5, A67, A73, A75, A77, RFUNCT_2:22; ::_thesis: verum
end;
 min (r,(g - p)) <= r by XXREAL_0:17;
then A78: (min (r,(g - p))) / 2 < r by A72, XXREAL_0:2;
then A79: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;
 - r < - ((min (r,(g - p))) / 2) by A78, XREAL_1:24;
then A80: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
 g < g + r by A69, XREAL_1:29;
then  g - ((min (r,(g - p))) / 2) < g + r by A73, XXREAL_0:2;
then  g - ((min (r,(g - p))) / 2) in  {  s where s is Real : ( g - r < s & s < g + r )  }  by A80;
then A81: g - ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def_2;
A82: x1 in X /\ (dom (f | X)) by A74, XBOOLE_0:def_4;
A83: g < g + ((min (r,(g - p))) / 2) by A71, XREAL_1:29, XREAL_1:215;
 x1 <> x0 by A67, A71, A75, XREAL_1:44, XREAL_1:215;
then  x1 < x0 by A76, XXREAL_0:1;
then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ as Neighbourhood of x0 by RCOMP_1:def_6, XREAL_1:50;
take N = N; ::_thesis: for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be Real; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A84: x in dom (f | X) and
A85: x in N ; ::_thesis: (f | X) . x in N1
 x in  {  s where s is Real : ( x0 - (x0 - x1) < s & s < x0 + (x0 - x1) )  }  by A85, RCOMP_1:def_2;
then A86: ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
 (f | X) . x in [.p,g.] by A3, A7, A84, FUNCT_1:def_6;
then  (f | X) . x in  {  s where s is Real : ( p <= s & s <= g )  }  by RCOMP_1:def_1;
then  ex s being Real st
( s = (f | X) . x & p <= s & s <= g ) ;
then A87: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A83, XXREAL_0:2;
 x in X /\ (dom (f | X)) by A84, XBOOLE_0:def_4;
then  g - ((min (r,(g - p))) / 2) <= (f | X) . x by A5, A75, A82, A86, RFUNCT_2:22;
then  (f | X) . x in  {  s where s is Real : ( g - ((min (r,(g - p))) / 2) <= s & s <= g + ((min (r,(g - p))) / 2) )  }  by A87;
then A88: (f | X) . x in [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] by RCOMP_1:def_1;
 g - r < g by A69, XREAL_1:44;
then  g - r < g + ((min (r,(g - p))) / 2) by A83, XXREAL_0:2;
then  g + ((min (r,(g - p))) / 2) in  {  s where s is Real : ( g - r < s & s < g + r )  }  by A79;
then  g + ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def_2;
then  [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] c= N1 by A70, A81, XXREAL_2:def_12;
hence  (f | X) . x in N1 by A88; ::_thesis: verum
end;
end;
end;
then consider N being Neighbourhood of x0 such that
A89: for x1 being Real st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1 ;
take N = N; ::_thesis: for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1
thus  for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1 by A89; ::_thesis: verum
end;
hence  f | X is_continuous_in x0 by Th4; ::_thesis: verum
end;
hence  f | X is continuous by Def2; ::_thesis: verum
end;
suppose f | X is non-increasing ; ::_thesis: f | X is continuous
then A90: (f | X) | X is non-increasing ;
 for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
A91: [.p,g.] = ].p,g.[ \/ {p,g} by A2, XXREAL_1:128;
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A92: (f | X) .: X = f .: X by RELAT_1:129;
assume A93: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
A94: (f | X) . x0 in (f | X) .: X by A93, FUNCT_1:def_6;
reconsider x0 = x0 as Real by XREAL_0:def_1;
 (f | X) . x0 in [.p,g.] by A3, A94, RELAT_1:129;
then A95: ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 in {p,g} ) by A91, XBOOLE_0:def_3;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x1_being_real_number_st_x1_in_dom_(f_|_X)_&_x1_in_N_holds_
(f_|_X)_._x1_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1
now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_Real_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
percases ( (f | X) . x0 in ].p,g.[ or (f | X) . x0 = p or (f | X) . x0 = g ) by A95, TARSKI:def_2;
suppose (f | X) . x0 in ].p,g.[ ; ::_thesis: ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider N2 being Neighbourhood of (f | X) . x0 such that
A96: N2 c= ].p,g.[ by RCOMP_1:18;
A97: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider N3 being Neighbourhood of (f | X) . x0 such that
A98: N3 c= N1 and
A99: N3 c= N2 by RCOMP_1:17;
consider r being real number  such that
A100: r > 0 and
A101: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A102: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A103: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;
A104: (f | X) . x0 < ((f | X) . x0) + r by A100, XREAL_1:29;
then  ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then  ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A103, XXREAL_0:2;
then  ((f | X) . x0) + (r / 2) in  {  s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r )  }  by A102;
then A105: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_2;
then  ((f | X) . x0) + (r / 2) in N2 by A99, A101;
then  ((f | X) . x0) + (r / 2) in ].p,g.[ by A96;
then consider x2 being Real such that
A106: ( x2 in dom (f | X) & x2 in X ) and
A107: ((f | X) . x0) + (r / 2) = (f | X) . x2 by A3, A92, A97, PARTFUN2:59;
A108: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
set M1 = ((f | X) . x0) - (r / 2);
A109: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;
 ((f | X) . x0) - (r / 2) < (f | X) . x0 by A103, XREAL_1:19;
then  ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A104, XXREAL_0:2;
then  ((f | X) . x0) - (r / 2) in  {  s where s is Real : ( ((f | X) . x0) - r < s & s < ((f | X) . x0) + r )  }  by A109;
then A110: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_2;
then  ((f | X) . x0) - (r / 2) in N2 by A99, A101;
then  ((f | X) . x0) - (r / 2) in ].p,g.[ by A96;
then consider x1 being Real such that
A111: ( x1 in dom (f | X) & x1 in X ) and
A112: ((f | X) . x0) - (r / 2) = (f | X) . x1 by A3, A92, A108, PARTFUN2:59;
A113: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A100, XREAL_1:29, XREAL_1:215;
then A114: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A115: now__::_thesis:_not_x0_>_x1
assume A116: x0 > x1 ; ::_thesis: contradiction
 ( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A111, XBOOLE_0:def_4;
hence  contradiction by A90, A112, A114, A116, RFUNCT_2:23; ::_thesis: verum
end;
A117: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A100, XREAL_1:29, XREAL_1:215;
A118: now__::_thesis:_not_x2_>_x0
assume A119: x2 > x0 ; ::_thesis: contradiction
 ( x0 in X /\ (dom (f | X)) & x2 in X /\ (dom (f | X)) ) by A93, A106, XBOOLE_0:def_4;
hence  contradiction by A90, A107, A117, A119, RFUNCT_2:23; ::_thesis: verum
end;
 x0 <> x2 by A100, A107, XREAL_1:29, XREAL_1:215;
then  x0 > x2 by A118, XXREAL_0:1;
then A120: x0 - x2 > 0 by XREAL_1:50;
set R = min ((x1 - x0),(x0 - x2));
A121: min ((x1 - x0),(x0 - x2)) <= x1 - x0 by XXREAL_0:17;
 x1 <> x0 by A112, A113, XREAL_1:19;
then  x1 > x0 by A115, XXREAL_0:1;
then  x1 - x0 > 0 by XREAL_1:50;
then  min ((x1 - x0),(x0 - x2)) > 0 by A120, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((x1 - x0),(x0 - x2)))),(x0 + (min ((x1 - x0),(x0 - x2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be Real; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A122: x in dom (f | X) and
A123: x in N ; ::_thesis: (f | X) . x in N1
A124: x in X /\ (dom (f | X)) by A122, XBOOLE_1:28;
 x in  {  s where s is Real : ( x0 - (min ((x1 - x0),(x0 - x2))) < s & s < x0 + (min ((x1 - x0),(x0 - x2))) )  }  by A123, RCOMP_1:def_2;
then A125: ex s being Real st
( s = x & x0 - (min ((x1 - x0),(x0 - x2))) < s & s < x0 + (min ((x1 - x0),(x0 - x2))) ) ;
then  x0 < (min ((x1 - x0),(x0 - x2))) + x by XREAL_1:19;
then A126: x0 - x < ((min ((x1 - x0),(x0 - x2))) + x) - x by XREAL_1:9;
 x - x0 < min ((x1 - x0),(x0 - x2)) by A125, XREAL_1:19;
then  x - x0 < x1 - x0 by A121, XXREAL_0:2;
then A127: (x - x0) + x0 < (x1 - x0) + x0 by XREAL_1:6;
 x1 in X /\ (dom (f | X)) by A111, XBOOLE_0:def_4;
then A128: (f | X) . x1 <= (f | X) . x by A90, A127, A124, RFUNCT_2:23;
 min ((x1 - x0),(x0 - x2)) <= x0 - x2 by XXREAL_0:17;
then  x0 - x < x0 - x2 by A126, XXREAL_0:2;
then  - (x0 - x) > - (x0 - x2) by XREAL_1:24;
then A129: (x - x0) + x0 > (x2 - x0) + x0 by XREAL_1:6;
 x2 in X /\ (dom (f | X)) by A106, XBOOLE_0:def_4;
then  (f | X) . x <= (f | X) . x2 by A90, A129, A124, RFUNCT_2:23;
then  (f | X) . x in  {  s where s is Real : ( ((f | X) . x0) - (r / 2) <= s & s <= ((f | X) . x0) + (r / 2) )  }  by A112, A107, A128;
then A130: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by RCOMP_1:def_1;
 [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A110, A105, XXREAL_2:def_12;
then  (f | X) . x in N3 by A101, A130;
hence  (f | X) . x in N1 by A98; ::_thesis: verum
end;
supposeA131: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider r being real number  such that
A132: r > 0 and
A133: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
set R = (min (r,(g - p))) / 2;
 g - p > 0 by A4, XREAL_1:50;
then A134: min (r,(g - p)) > 0 by A132, XXREAL_0:15;
then A135: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
 min (r,(g - p)) <= r by XXREAL_0:17;
then A136: (min (r,(g - p))) / 2 < r by A135, XXREAL_0:2;
then A137: p + ((min (r,(g - p))) / 2) < p + r by XREAL_1:6;
A138: p - ((min (r,(g - p))) / 2) < p by A134, XREAL_1:44, XREAL_1:215;
 - r < - ((min (r,(g - p))) / 2) by A136, XREAL_1:24;
then A139: p + (- r) < p + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
 p < p + r by A132, XREAL_1:29;
then  p - ((min (r,(g - p))) / 2) < p + r by A138, XXREAL_0:2;
then  p - ((min (r,(g - p))) / 2) in  {  s where s is Real : ( p - r < s & s < p + r )  }  by A139;
then A140: p - ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def_2;
A141: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
A142: p < p + ((min (r,(g - p))) / 2) by A134, XREAL_1:29, XREAL_1:215;
 min (r,(g - p)) <= g - p by XXREAL_0:17;
then  (min (r,(g - p))) / 2 < g - p by A135, XXREAL_0:2;
then  p + ((min (r,(g - p))) / 2) < g by XREAL_1:20;
then  p + ((min (r,(g - p))) / 2) in  {  s where s is Real : ( p < s & s < g )  }  by A142;
then  p + ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def_2;
then consider x1 being Real such that
A143: ( x1 in dom (f | X) & x1 in X ) and
A144: p + ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A92, A141, PARTFUN2:59;
A145: x1 in X /\ (dom (f | X)) by A143, XBOOLE_0:def_4;
now__::_thesis:_not_x1_>_x0
assume A146: x1 > x0 ; ::_thesis: contradiction
 ( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A143, XBOOLE_0:def_4;
hence  contradiction by A90, A131, A142, A144, A146, RFUNCT_2:23; ::_thesis: verum
end;
then  x0 > x1 by A131, A142, A144, XXREAL_0:1;
then reconsider N = ].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ as Neighbourhood of x0 by RCOMP_1:def_6, XREAL_1:50;
take N = N; ::_thesis: for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be Real; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A147: x in dom (f | X) and
A148: x in N ; ::_thesis: (f | X) . x in N1
 x in  {  s where s is Real : ( x0 - (x0 - x1) < s & s < x0 + (x0 - x1) )  }  by A148, RCOMP_1:def_2;
then A149: ex s being Real st
( s = x & x0 - (x0 - x1) < s & s < x0 + (x0 - x1) ) ;
 (f | X) . x in [.p,g.] by A3, A92, A147, FUNCT_1:def_6;
then  (f | X) . x in  {  s where s is Real : ( p <= s & s <= g )  }  by RCOMP_1:def_1;
then  ex s being Real st
( s = (f | X) . x & p <= s & s <= g ) ;
then A150: p - ((min (r,(g - p))) / 2) <= (f | X) . x by A138, XXREAL_0:2;
 x in X /\ (dom (f | X)) by A147, XBOOLE_0:def_4;
then  (f | X) . x <= p + ((min (r,(g - p))) / 2) by A90, A144, A145, A149, RFUNCT_2:23;
then  (f | X) . x in  {  s where s is Real : ( p - ((min (r,(g - p))) / 2) <= s & s <= p + ((min (r,(g - p))) / 2) )  }  by A150;
then A151: (f | X) . x in [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] by RCOMP_1:def_1;
 p - r < p by A132, XREAL_1:44;
then  p - r < p + ((min (r,(g - p))) / 2) by A142, XXREAL_0:2;
then  p + ((min (r,(g - p))) / 2) in  {  s where s is Real : ( p - r < s & s < p + r )  }  by A137;
then  p + ((min (r,(g - p))) / 2) in ].(p - r),(p + r).[ by RCOMP_1:def_2;
then  [.(p - ((min (r,(g - p))) / 2)),(p + ((min (r,(g - p))) / 2)).] c= N1 by A133, A140, XXREAL_2:def_12;
hence  (f | X) . x in N1 by A151; ::_thesis: verum
end;
supposeA152: (f | X) . x0 = g ; ::_thesis: ex N being Neighbourhood of x0 st
for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
A153: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider r being real number  such that
A154: r > 0 and
A155: N1 = ].(g - r),(g + r).[ by A152, RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
set R = (min (r,(g - p))) / 2;
 g - p > 0 by A4, XREAL_1:50;
then A156: min (r,(g - p)) > 0 by A154, XXREAL_0:15;
then A157: (min (r,(g - p))) / 2 < min (r,(g - p)) by XREAL_1:216;
A158: g - ((min (r,(g - p))) / 2) < g by A156, XREAL_1:44, XREAL_1:215;
 min (r,(g - p)) <= g - p by XXREAL_0:17;
then  (min (r,(g - p))) / 2 < g - p by A157, XXREAL_0:2;
then  ((min (r,(g - p))) / 2) + p < g by XREAL_1:20;
then  g - ((min (r,(g - p))) / 2) > p by XREAL_1:20;
then  g - ((min (r,(g - p))) / 2) in  {  s where s is Real : ( p < s & s < g )  }  by A158;
then  g - ((min (r,(g - p))) / 2) in ].p,g.[ by RCOMP_1:def_2;
then consider x1 being Real such that
A159: ( x1 in dom (f | X) & x1 in X ) and
A160: g - ((min (r,(g - p))) / 2) = (f | X) . x1 by A3, A92, A153, PARTFUN2:59;
A161: now__::_thesis:_not_x0_>_x1
assume A162: x0 > x1 ; ::_thesis: contradiction
 ( x0 in X /\ (dom (f | X)) & x1 in X /\ (dom (f | X)) ) by A93, A159, XBOOLE_0:def_4;
hence  contradiction by A90, A152, A158, A160, A162, RFUNCT_2:23; ::_thesis: verum
end;
 min (r,(g - p)) <= r by XXREAL_0:17;
then A163: (min (r,(g - p))) / 2 < r by A157, XXREAL_0:2;
then A164: g + ((min (r,(g - p))) / 2) < g + r by XREAL_1:6;
 - r < - ((min (r,(g - p))) / 2) by A163, XREAL_1:24;
then A165: g + (- r) < g + (- ((min (r,(g - p))) / 2)) by XREAL_1:6;
 g < g + r by A154, XREAL_1:29;
then  g - ((min (r,(g - p))) / 2) < g + r by A158, XXREAL_0:2;
then  g - ((min (r,(g - p))) / 2) in  {  s where s is Real : ( g - r < s & s < g + r )  }  by A165;
then A166: g - ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def_2;
A167: x1 in X /\ (dom (f | X)) by A159, XBOOLE_0:def_4;
A168: g < g + ((min (r,(g - p))) / 2) by A156, XREAL_1:29, XREAL_1:215;
 x1 <> x0 by A152, A156, A160, XREAL_1:44, XREAL_1:215;
then  x1 > x0 by A161, XXREAL_0:1;
then reconsider N = ].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def_6, XREAL_1:50;
take N = N; ::_thesis: for x being Real st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be Real; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A169: x in dom (f | X) and
A170: x in N ; ::_thesis: (f | X) . x in N1
 x in  {  s where s is Real : ( x0 - (x1 - x0) < s & s < x0 + (x1 - x0) )  }  by A170, RCOMP_1:def_2;
then A171: ex s being Real st
( s = x & x0 - (x1 - x0) < s & s < x0 + (x1 - x0) ) ;
 (f | X) . x in [.p,g.] by A3, A92, A169, FUNCT_1:def_6;
then  (f | X) . x in  {  s where s is Real : ( p <= s & s <= g )  }  by RCOMP_1:def_1;
then  ex s being Real st
( s = (f | X) . x & p <= s & s <= g ) ;
then A172: (f | X) . x <= g + ((min (r,(g - p))) / 2) by A168, XXREAL_0:2;
 x in X /\ (dom (f | X)) by A169, XBOOLE_0:def_4;
then  g - ((min (r,(g - p))) / 2) <= (f | X) . x by A90, A160, A167, A171, RFUNCT_2:23;
then  (f | X) . x in  {  s where s is Real : ( g - ((min (r,(g - p))) / 2) <= s & s <= g + ((min (r,(g - p))) / 2) )  }  by A172;
then A173: (f | X) . x in [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] by RCOMP_1:def_1;
 g - r < g by A154, XREAL_1:44;
then  g - r < g + ((min (r,(g - p))) / 2) by A168, XXREAL_0:2;
then  g + ((min (r,(g - p))) / 2) in  {  s where s is Real : ( g - r < s & s < g + r )  }  by A164;
then  g + ((min (r,(g - p))) / 2) in ].(g - r),(g + r).[ by RCOMP_1:def_2;
then  [.(g - ((min (r,(g - p))) / 2)),(g + ((min (r,(g - p))) / 2)).] c= N1 by A155, A166, XXREAL_2:def_12;
hence  (f | X) . x in N1 by A173; ::_thesis: verum
end;
end;
end;
then consider N being Neighbourhood of x0 such that
A174: for x1 being Real st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1 ;
take N = N; ::_thesis: for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1
thus  for x1 being real number st x1 in dom (f | X) & x1 in N holds
(f | X) . x1 in N1 by A174; ::_thesis: verum
end;
hence  f | X is_continuous_in x0 by Th4; ::_thesis: verum
end;
hence  f | X is continuous by Def2; ::_thesis: verum
end;
end;
end;
hence  f | X is continuous ; ::_thesis: verum
end;
end;
end;
hence  f | X is continuous ; ::_thesis: verum
end;

theorem :: FCONT_1:47
for p, g being real number
for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) holds
((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous
proof
let p, g be real number ; ::_thesis: for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) holds
((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( p <= g & [.p,g.] c= dom f & ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) implies ((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous )
assume that
A1: p <= g and
A2: [.p,g.] c= dom f and
A3: ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) ; ::_thesis: ((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous
reconsider p = p, g = g as Real by XREAL_0:def_1;
now__::_thesis:_((f_|_[.p,g.])_")_|_(f_.:_[.p,g.])_is_continuous
percases ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) by A3;
supposeA4: f | [.p,g.] is increasing ; ::_thesis: ((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous
A5: ((f | [.p,g.]) ") .: (f .: [.p,g.]) = ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115
.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33
.= rng ((f | [.p,g.]) ") by RELAT_1:113
.= dom (f | [.p,g.]) by FUNCT_1:33
.= (dom f) /\ [.p,g.] by RELAT_1:61
.= [.p,g.] by A2, XBOOLE_1:28 ;
 ((f | [.p,g.]) ") | (f .: [.p,g.]) is increasing by A4, RFUNCT_2:51;
hence  ((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous by A1, A5, Th46; ::_thesis: verum
end;
supposeA6: f | [.p,g.] is decreasing ; ::_thesis: ((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous
A7: ((f | [.p,g.]) ") .: (f .: [.p,g.]) = ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115
.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33
.= rng ((f | [.p,g.]) ") by RELAT_1:113
.= dom (f | [.p,g.]) by FUNCT_1:33
.= (dom f) /\ [.p,g.] by RELAT_1:61
.= [.p,g.] by A2, XBOOLE_1:28 ;
 ((f | [.p,g.]) ") | (f .: [.p,g.]) is decreasing by A6, RFUNCT_2:52;
hence  ((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous by A1, A7, Th46; ::_thesis: verum
end;
end;
end;
hence  ((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous ; ::_thesis: verum
end;

definition
let a, b be real number ;
func AffineMap (a,b) ->  Function of REAL,REAL means :Def4: :: FCONT_1:def 4
 for x being real number holds it . x = (a * x) + b;
existence
 ex b1 being Function of REAL,REAL st
for x being real number holds b1 . x = (a * x) + b
proof
reconsider a9 = a, b9 = b as Element of REAL by XREAL_0:def_1;
deffunc H1( Real) ->  Element of REAL = (a9 * $1) + b9;
consider f being Function of REAL,REAL such that
A1: for x being Element of REAL holds f . x = H1(x) from FUNCT_2:sch_4();
take  f ; ::_thesis: for x being real number holds f . x = (a * x) + b
let x be real number ; ::_thesis: f . x = (a * x) + b
reconsider x9 = x as Element of REAL by XREAL_0:def_1;
 f . x9 = (a9 * x) + b9 by A1;
hence  f . x = (a * x) + b ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for x being real number holds b1 . x = (a * x) + b ) & ( for x being real number holds b2 . x = (a * x) + b ) holds
b1 = b2
proof
let f, f9 be Function of REAL,REAL; ::_thesis: ( ( for x being real number holds f . x = (a * x) + b ) & ( for x being real number holds f9 . x = (a * x) + b ) implies f = f9 )
assume that
A2: for x being real number holds f . x = (a * x) + b and
A3: for x being real number holds f9 . x = (a * x) + b ; ::_thesis: f = f9
now__::_thesis:_for_x_being_Element_of_REAL_holds_f_._x_=_f9_._x
let x be Element of REAL ; ::_thesis: f . x = f9 . x
thus f . x = (a * x) + b by A2
.= f9 . x by A3 ; ::_thesis: verum
end;
hence  f = f9 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines AffineMap FCONT_1:def_4_:_
 for a, b being real number
for b3 being Function of REAL,REAL holds
( b3 = AffineMap (a,b) iff for x being real number holds b3 . x = (a * x) + b );

registration
let a, b be real number ;
cluster AffineMap (a,b) ->  continuous ;
coherence
 AffineMap (a,b) is continuous
proof
set f = AffineMap (a,b);
 for x0 being real number st x0 in REAL holds
(AffineMap (a,b)) . x0 = (a * x0) + b by Def4;
then  ( REAL = dom (AffineMap (a,b)) & (AffineMap (a,b)) | REAL is continuous ) by Th41, FUNCT_2:def_1;
hence  AffineMap (a,b) is continuous ; ::_thesis: verum
end;
end;

registration
cluster Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous for Element of bool [:REAL,REAL:];
existence
 ex b1 being Function of REAL,REAL st b1 is continuous
proof
take  AffineMap (1,1) ; ::_thesis: AffineMap (1,1) is continuous
thus  AffineMap (1,1) is continuous ; ::_thesis: verum
end;
end;

theorem Th48: :: FCONT_1:48
for a, b being real number holds (AffineMap (a,b)) . 0 = b
proof
let a, b be real number ; ::_thesis: (AffineMap (a,b)) . 0 = b
thus (AffineMap (a,b)) . 0 = (a * 0) + b by Def4
.= b ; ::_thesis: verum
end;

theorem Th49: :: FCONT_1:49
for a, b being real number holds (AffineMap (a,b)) . 1 = a + b
proof
let a, b be real number ; ::_thesis: (AffineMap (a,b)) . 1 = a + b
thus (AffineMap (a,b)) . 1 = (a * 1) + b by Def4
.= a + b ; ::_thesis: verum
end;

theorem Th50: :: FCONT_1:50
for a, b being real number st a <> 0 holds
AffineMap (a,b) is one-to-one
proof
let a, b be real number ; ::_thesis: ( a <> 0 implies AffineMap (a,b) is one-to-one )
assume A1: a <> 0 ; ::_thesis: AffineMap (a,b) is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (AffineMap (a,b)) or not x2 in dom (AffineMap (a,b)) or not (AffineMap (a,b)) . x1 = (AffineMap (a,b)) . x2 or x1 = x2 )
set f = AffineMap (a,b);
assume  x1 in dom (AffineMap (a,b)) ; ::_thesis: ( not x2 in dom (AffineMap (a,b)) or not (AffineMap (a,b)) . x1 = (AffineMap (a,b)) . x2 or x1 = x2 )
then reconsider r1 = x1 as real number ;
assume  x2 in dom (AffineMap (a,b)) ; ::_thesis: ( not (AffineMap (a,b)) . x1 = (AffineMap (a,b)) . x2 or x1 = x2 )
then reconsider r2 = x2 as real number ;
assume  (AffineMap (a,b)) . x1 = (AffineMap (a,b)) . x2 ; ::_thesis: x1 = x2
then (a * r1) + b = (AffineMap (a,b)) . x2 by Def4
.= (a * r2) + b by Def4 ;
hence  x1 = x2 by A1, XCMPLX_1:5; ::_thesis: verum
end;

theorem :: FCONT_1:51
for a, b, x, y being real number st a > 0 & x < y holds
(AffineMap (a,b)) . x < (AffineMap (a,b)) . y
proof
let a, b, x, y be real number ; ::_thesis: ( a > 0 & x < y implies (AffineMap (a,b)) . x < (AffineMap (a,b)) . y )
assume  ( a > 0 & x < y ) ; ::_thesis: (AffineMap (a,b)) . x < (AffineMap (a,b)) . y
then A1: a * x < a * y by XREAL_1:68;
 ( (AffineMap (a,b)) . x = (a * x) + b & (AffineMap (a,b)) . y = (a * y) + b ) by Def4;
hence  (AffineMap (a,b)) . x < (AffineMap (a,b)) . y by A1, XREAL_1:8; ::_thesis: verum
end;

theorem :: FCONT_1:52
for a, b, x, y being real number st a < 0 & x < y holds
(AffineMap (a,b)) . x > (AffineMap (a,b)) . y
proof
let a, b, x, y be real number ; ::_thesis: ( a < 0 & x < y implies (AffineMap (a,b)) . x > (AffineMap (a,b)) . y )
assume  ( a < 0 & x < y ) ; ::_thesis: (AffineMap (a,b)) . x > (AffineMap (a,b)) . y
then A1: a * x > a * y by XREAL_1:69;
 ( (AffineMap (a,b)) . x = (a * x) + b & (AffineMap (a,b)) . y = (a * y) + b ) by Def4;
hence  (AffineMap (a,b)) . x > (AffineMap (a,b)) . y by A1, XREAL_1:8; ::_thesis: verum
end;

theorem Th53: :: FCONT_1:53
for a, b, x, y being real number st a >= 0 & x <= y holds
(AffineMap (a,b)) . x <= (AffineMap (a,b)) . y
proof
let a, b, x, y be real number ; ::_thesis: ( a >= 0 & x <= y implies (AffineMap (a,b)) . x <= (AffineMap (a,b)) . y )
assume  ( a >= 0 & x <= y ) ; ::_thesis: (AffineMap (a,b)) . x <= (AffineMap (a,b)) . y
then A1: a * x <= a * y by XREAL_1:64;
 ( (AffineMap (a,b)) . x = (a * x) + b & (AffineMap (a,b)) . y = (a * y) + b ) by Def4;
hence  (AffineMap (a,b)) . x <= (AffineMap (a,b)) . y by A1, XREAL_1:7; ::_thesis: verum
end;

theorem :: FCONT_1:54
for a, b, x, y being real number st a <= 0 & x <= y holds
(AffineMap (a,b)) . x >= (AffineMap (a,b)) . y
proof
let a, b, x, y be real number ; ::_thesis: ( a <= 0 & x <= y implies (AffineMap (a,b)) . x >= (AffineMap (a,b)) . y )
assume  ( a <= 0 & x <= y ) ; ::_thesis: (AffineMap (a,b)) . x >= (AffineMap (a,b)) . y
then A1: a * x >= a * y by XREAL_1:65;
 ( (AffineMap (a,b)) . x = (a * x) + b & (AffineMap (a,b)) . y = (a * y) + b ) by Def4;
hence  (AffineMap (a,b)) . x >= (AffineMap (a,b)) . y by A1, XREAL_1:7; ::_thesis: verum
end;

theorem Th55: :: FCONT_1:55
for a, b being real number st a <> 0 holds
rng (AffineMap (a,b)) = REAL
proof
let a, b be real number ; ::_thesis: ( a <> 0 implies rng (AffineMap (a,b)) = REAL )
assume A1: a <> 0 ; ::_thesis: rng (AffineMap (a,b)) = REAL
thus  rng (AffineMap (a,b)) c= REAL ; :: according to XBOOLE_0:def_10 ::_thesis: REAL c= rng (AffineMap (a,b))
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in REAL or e in rng (AffineMap (a,b)) )
assume  e in REAL ; ::_thesis: e in rng (AffineMap (a,b))
then reconsider r = e as Element of REAL ;
set s = (r - b) / a;
(AffineMap (a,b)) . ((r - b) / a) = (a * ((r - b) / a)) + b by Def4
.= (r - b) + b by A1, XCMPLX_1:87
.= r ;
hence  e in rng (AffineMap (a,b)) by FUNCT_2:4; ::_thesis: verum
end;

theorem :: FCONT_1:56
for a, b being real number st a <> 0 holds
(AffineMap (a,b)) " = AffineMap ((a "),(- (b / a)))
proof
let a, b be real number ; ::_thesis: ( a <> 0 implies (AffineMap (a,b)) " = AffineMap ((a "),(- (b / a))) )
assume A1: a <> 0 ; ::_thesis: (AffineMap (a,b)) " = AffineMap ((a "),(- (b / a)))
 for x being Element of REAL holds ((AffineMap ((a "),(- (b / a)))) * (AffineMap (a,b))) . x = (id REAL) . x
proof
let x be Element of REAL ; ::_thesis: ((AffineMap ((a "),(- (b / a)))) * (AffineMap (a,b))) . x = (id REAL) . x
thus ((AffineMap ((a "),(- (b / a)))) * (AffineMap (a,b))) . x = (AffineMap ((a "),(- (b / a)))) . ((AffineMap (a,b)) . x) by FUNCT_2:15
.= (AffineMap ((a "),(- (b / a)))) . ((a * x) + b) by Def4
.= ((a ") * ((a * x) + b)) + (- (b / a)) by Def4
.= ((((a ") * a) * x) + ((a ") * b)) + (- (b / a))
.= ((1 * x) + ((a ") * b)) + (- (b / a)) by A1, XCMPLX_0:def_7
.= (x + ((a ") * b)) - (b / a)
.= (x + (b / a)) - (b / a) by XCMPLX_0:def_9
.= (id REAL) . x by FUNCT_1:18 ; ::_thesis: verum
end;
then A2: (AffineMap ((a "),(- (b / a)))) * (AffineMap (a,b)) = id REAL by FUNCT_2:63;
 rng (AffineMap (a,b)) = REAL by A1, Th55;
hence  (AffineMap (a,b)) " = AffineMap ((a "),(- (b / a))) by A1, A2, Th50, FUNCT_2:30; ::_thesis: verum
end;

theorem :: FCONT_1:57
for a, b being real number st a > 0 holds
(AffineMap (a,b)) .: [.0,1.] = [.b,(a + b).]
proof
let a, b be real number ; ::_thesis: ( a > 0 implies (AffineMap (a,b)) .: [.0,1.] = [.b,(a + b).] )
assume A1: a > 0 ; ::_thesis: (AffineMap (a,b)) .: [.0,1.] = [.b,(a + b).]
thus  (AffineMap (a,b)) .: [.0,1.] c= [.b,(a + b).] :: according to XBOOLE_0:def_10 ::_thesis: [.b,(a + b).] c= (AffineMap (a,b)) .: [.0,1.]
proof
A2: (AffineMap (a,b)) . 1 = a + b by Th49;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in (AffineMap (a,b)) .: [.0,1.] or u in [.b,(a + b).] )
assume  u in (AffineMap (a,b)) .: [.0,1.] ; ::_thesis: u in [.b,(a + b).]
then consider r being Element of REAL  such that
A3: r in [.0,1.] and
A4: u = (AffineMap (a,b)) . r by FUNCT_2:65;
reconsider s = u as real number by A4;
 r <= 1 by A3, XXREAL_1:1;
then A5: s <= a + b by A1, A4, A2, Th53;
A6: (AffineMap (a,b)) . 0 = b by Th48;
 0 <= r by A3, XXREAL_1:1;
then  b <= s by A1, A4, A6, Th53;
hence  u in [.b,(a + b).] by A5, XXREAL_1:1; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in [.b,(a + b).] or u in (AffineMap (a,b)) .: [.0,1.] )
assume A7: u in [.b,(a + b).] ; ::_thesis: u in (AffineMap (a,b)) .: [.0,1.]
then reconsider r = u as Element of REAL ;
set s = (r - b) / a;
A8: (AffineMap (a,b)) . ((r - b) / a) = (a * ((r - b) / a)) + b by Def4
.= (r - b) + b by A1, XCMPLX_1:87
.= r ;
 r <= a + b by A7, XXREAL_1:1;
then  r - b <= a by XREAL_1:20;
then  (r - b) / a <= a / a by A1, XREAL_1:72;
then A9: (r - b) / a <= 1 by A1, XCMPLX_1:60;
 b <= r by A7, XXREAL_1:1;
then  0 <= r - b by XREAL_1:48;
then  (r - b) / a in [.0,1.] by A1, A9, XXREAL_1:1;
hence  u in (AffineMap (a,b)) .: [.0,1.] by A8, FUNCT_2:35; ::_thesis: verum
end;