let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL holds

( f is_continuous_in x0 iff for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

let f be PartFunc of REAL,REAL; :: thesis: ( f is_continuous_in x0 iff for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

thus ( f is_continuous_in x0 implies for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) :: thesis: ( ( for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) implies f is_continuous_in x0 )

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ; :: thesis: f is_continuous_in x0

( f is_continuous_in x0 iff for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

let f be PartFunc of REAL,REAL; :: thesis: ( f is_continuous_in x0 iff for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) )

thus ( f is_continuous_in x0 implies for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) :: thesis: ( ( for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) ) ) implies f is_continuous_in x0 )

proof

assume A17:
for r being Real st 0 < r holds
assume A1:
f is_continuous_in x0
; :: thesis: for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) )

given r being Real such that A2: 0 < r and

A3: for s being Real holds

( not 0 < s or ex x1 being Real st

( x1 in dom f & |.(x1 - x0).| < s & not |.((f . x1) - (f . x0)).| < r ) ) ; :: thesis: contradiction

defpred S_{1}[ Element of NAT , Real] means ( $2 in dom f & |.($2 - x0).| < 1 / ($1 + 1) & not |.((f . $2) - (f . x0)).| < r );

A4: for n being Element of NAT ex p being Element of REAL st S_{1}[n,p]

A6: for n being Element of NAT holds S_{1}[n,s1 . n]
from FUNCT_2:sch 3(A4);

A7: rng s1 c= dom f

then lim s1 = x0 by A10, SEQ_2:def 7;

then ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A1, A7, A15;

then consider n being Nat such that

A16: for m being Nat st n <= m holds

|.(((f /* s1) . m) - (f . x0)).| < r by A2, SEQ_2:def 7;

|.(((f /* s1) . n) - (f . x0)).| < r by A16;

hence contradiction by A8; :: thesis: verum

end;ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < r ) )

given r being Real such that A2: 0 < r and

A3: for s being Real holds

( not 0 < s or ex x1 being Real st

( x1 in dom f & |.(x1 - x0).| < s & not |.((f . x1) - (f . x0)).| < r ) ) ; :: thesis: contradiction

defpred S

A4: for n being Element of NAT ex p being Element of REAL st S

proof

consider s1 being Real_Sequence such that
let n be Element of NAT ; :: thesis: ex p being Element of REAL st S_{1}[n,p]

0 < (n + 1) " ;

then 0 < 1 / (n + 1) by XCMPLX_1:215;

then consider p being Real such that

A5: ( p in dom f & |.(p - x0).| < 1 / (n + 1) & not |.((f . p) - (f . x0)).| < r ) by A3;

take p ; :: thesis: ( p is set & p is Element of REAL & S_{1}[n,p] )

thus ( p is set & p is Element of REAL & S_{1}[n,p] )
by A5; :: thesis: verum

end;0 < (n + 1) " ;

then 0 < 1 / (n + 1) by XCMPLX_1:215;

then consider p being Real such that

A5: ( p in dom f & |.(p - x0).| < 1 / (n + 1) & not |.((f . p) - (f . x0)).| < r ) by A3;

take p ; :: thesis: ( p is set & p is Element of REAL & S

thus ( p is set & p is Element of REAL & S

A6: for n being Element of NAT holds S

A7: rng s1 c= dom f

proof

let x be object ; :: 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;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

A8: now :: thesis: for n being Nat holds not |.(((f /* s1) . n) - (f . x0)).| < r

let n be Nat; :: thesis: not |.(((f /* s1) . n) - (f . x0)).| < r

A9: n in NAT by ORDINAL1:def 12;

not |.((f . (s1 . n)) - (f . x0)).| < r by A6, A9;

hence not |.(((f /* s1) . n) - (f . x0)).| < r by A7, FUNCT_2:108, A9; :: thesis: verum

end;A9: n in NAT by ORDINAL1:def 12;

not |.((f . (s1 . n)) - (f . x0)).| < r by A6, A9;

hence not |.(((f /* s1) . n) - (f . x0)).| < r by A7, FUNCT_2:108, A9; :: thesis: verum

A10: now :: thesis: for s being Real st 0 < s holds

ex k being Nat st

for m being Nat st k <= m holds

|.((s1 . m) - x0).| < s

then A15:
s1 is convergent
by SEQ_2:def 6;ex k being Nat st

for m being Nat st k <= m holds

|.((s1 . m) - x0).| < s

let s be Real; :: thesis: ( 0 < s implies ex k being Nat st

for m being Nat st k <= m holds

|.((s1 . m) - x0).| < s )

assume A11: 0 < s ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.((s1 . m) - x0).| < s

consider n being Nat such that

A12: s " < n by SEQ_4:3;

(s ") + 0 < n + 1 by A12, XREAL_1:8;

then 1 / (n + 1) < 1 / (s ") by A11, XREAL_1:76;

then A13: 1 / (n + 1) < s by XCMPLX_1:216;

take k = n; :: thesis: for m being Nat st k <= m holds

|.((s1 . m) - x0).| < s

let m be Nat; :: thesis: ( k <= m implies |.((s1 . m) - x0).| < s )

A14: m in NAT by ORDINAL1:def 12;

assume k <= m ; :: thesis: |.((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 A13, XXREAL_0:2;

hence |.((s1 . m) - x0).| < s by A6, XXREAL_0:2, A14; :: thesis: verum

end;for m being Nat st k <= m holds

|.((s1 . m) - x0).| < s )

assume A11: 0 < s ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.((s1 . m) - x0).| < s

consider n being Nat such that

A12: s " < n by SEQ_4:3;

(s ") + 0 < n + 1 by A12, XREAL_1:8;

then 1 / (n + 1) < 1 / (s ") by A11, XREAL_1:76;

then A13: 1 / (n + 1) < s by XCMPLX_1:216;

take k = n; :: thesis: for m being Nat st k <= m holds

|.((s1 . m) - x0).| < s

let m be Nat; :: thesis: ( k <= m implies |.((s1 . m) - x0).| < s )

A14: m in NAT by ORDINAL1:def 12;

assume k <= m ; :: thesis: |.((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 A13, XXREAL_0:2;

hence |.((s1 . m) - x0).| < s by A6, XXREAL_0:2, A14; :: thesis: verum

then lim s1 = x0 by A10, SEQ_2:def 7;

then ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A1, A7, A15;

then consider n being Nat such that

A16: for m being Nat st n <= m holds

|.(((f /* s1) . m) - (f . x0)).| < r by A2, SEQ_2:def 7;

|.(((f /* s1) . n) - (f . x0)).| < r by A16;

hence contradiction by A8; :: thesis: verum

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((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) )

hence
f is_continuous_in x0
; :: thesis: verum( 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

A18: rng s1 c= dom f and

A19: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( f /* s1 is convergent & f . x0 = lim (f /* s1) )

hence ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A20, SEQ_2:def 7; :: thesis: verum

end;assume that

A18: rng s1 c= dom f and

A19: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( f /* s1 is convergent & f . x0 = lim (f /* s1) )

A20: now :: thesis: for p being Real st 0 < p holds

ex k being Nat st

for m being Nat st k <= m holds

|.(((f /* s1) . m) - (f . x0)).| < p

then
f /* s1 is convergent
by SEQ_2:def 6;ex k being Nat st

for m being Nat st k <= m holds

|.(((f /* s1) . m) - (f . x0)).| < p

let p be Real; :: thesis: ( 0 < p implies ex k being Nat st

for m being Nat st k <= m holds

|.(((f /* s1) . m) - (f . x0)).| < p )

assume 0 < p ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.(((f /* s1) . m) - (f . x0)).| < p

then consider s being Real such that

A21: 0 < s and

A22: for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < p by A17;

consider n being Nat such that

A23: for m being Nat st n <= m holds

|.((s1 . m) - x0).| < s by A19, A21, SEQ_2:def 7;

take k = n; :: thesis: for m being Nat st k <= m holds

|.(((f /* s1) . m) - (f . x0)).| < p

let m be Nat; :: thesis: ( k <= m implies |.(((f /* s1) . m) - (f . x0)).| < p )

A24: m in NAT by ORDINAL1:def 12;

assume k <= m ; :: thesis: |.(((f /* s1) . m) - (f . x0)).| < p

then ( s1 . m in rng s1 & |.((s1 . m) - x0).| < s ) by A23, VALUED_0:28;

then |.((f . (s1 . m)) - (f . x0)).| < p by A18, A22;

hence |.(((f /* s1) . m) - (f . x0)).| < p by A18, FUNCT_2:108, A24; :: thesis: verum

end;for m being Nat st k <= m holds

|.(((f /* s1) . m) - (f . x0)).| < p )

assume 0 < p ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.(((f /* s1) . m) - (f . x0)).| < p

then consider s being Real such that

A21: 0 < s and

A22: for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

|.((f . x1) - (f . x0)).| < p by A17;

consider n being Nat such that

A23: for m being Nat st n <= m holds

|.((s1 . m) - x0).| < s by A19, A21, SEQ_2:def 7;

take k = n; :: thesis: for m being Nat st k <= m holds

|.(((f /* s1) . m) - (f . x0)).| < p

let m be Nat; :: thesis: ( k <= m implies |.(((f /* s1) . m) - (f . x0)).| < p )

A24: m in NAT by ORDINAL1:def 12;

assume k <= m ; :: thesis: |.(((f /* s1) . m) - (f . x0)).| < p

then ( s1 . m in rng s1 & |.((s1 . m) - x0).| < s ) by A23, VALUED_0:28;

then |.((f . (s1 . m)) - (f . x0)).| < p by A18, A22;

hence |.(((f /* s1) . m) - (f . x0)).| < p by A18, FUNCT_2:108, A24; :: thesis: verum

hence ( f /* s1 is convergent & f . x0 = lim (f /* s1) ) by A20, SEQ_2:def 7; :: thesis: verum