let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

let f be PartFunc of S,T; :: thesis: for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

let x0 be Point of S; :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) ; :: thesis: ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) implies f is_continuous_in x0 )

assume that

A1: x0 in dom f and

A2: for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

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

thus x0 in dom f by A1; :: according to NFCONT_1:def 5 :: thesis: for b_{1} being Element of K16(K17(NAT, the carrier of S)) holds

( not rng b_{1} c= dom f or not b_{1} is convergent or not lim b_{1} = x0 or ( f /* b_{1} is convergent & f /. x0 = lim (f /* b_{1}) ) )

let s2 be sequence of S; :: thesis: ( not rng s2 c= dom f or not s2 is convergent or not lim s2 = x0 or ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) )

assume that

A3: rng s2 c= dom f and

A4: ( s2 is convergent & lim s2 = x0 ) ; :: thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

let f be PartFunc of S,T; :: thesis: for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

let x0 be Point of S; :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) ; :: thesis: ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) implies f is_continuous_in x0 )

assume that

A1: x0 in dom f and

A2: for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

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

thus x0 in dom f by A1; :: according to NFCONT_1:def 5 :: thesis: for b

( not rng b

let s2 be sequence of S; :: thesis: ( not rng s2 c= dom f or not s2 is convergent or not lim s2 = x0 or ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) )

assume that

A3: rng s2 c= dom f and

A4: ( 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) )end;

hence
( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
; :: thesis: verumper cases
( 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 ) ) ;

end;

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

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

A5: for m being Element of NAT st N <= m holds

s2 . m = x0 ;

A6: for n being Element of NAT holds (s2 ^\ N) . n = x0

A12: f /* (s2 ^\ N) = (f /* s2) ^\ N by A3, VALUED_0:27;

then A13: f /* s2 is convergent by A11, LOPBAN_3:10;

f /. x0 = lim ((f /* s2) ^\ N) by A8, A11, A12, NORMSP_1:def 7;

hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by A13, LOPBAN_3:9; :: thesis: verum

end;A5: for m being Element of NAT st N <= m holds

s2 . m = x0 ;

A6: for n being Element of NAT holds (s2 ^\ N) . n = x0

proof

A7:
rng (s2 ^\ N) c= rng s2
by VALUED_0:21;
let n be Element of NAT ; :: thesis: (s2 ^\ N) . n = x0

s2 . (n + N) = x0 by A5, NAT_1:12;

hence (s2 ^\ N) . n = x0 by NAT_1:def 3; :: thesis: verum

end;s2 . (n + N) = x0 by A5, NAT_1:12;

hence (s2 ^\ N) . n = x0 by NAT_1:def 3; :: thesis: verum

A8: now :: thesis: for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p

then A11:
f /* (s2 ^\ N) is convergent
;ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p

let p be Real; :: thesis: ( p > 0 implies ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p )

assume A9: p > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p

reconsider n = 0 as Nat ;

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

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p )

assume n <= m ; :: thesis: ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p

A10: m in NAT by ORDINAL1:def 12;

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| = ||.((f /. ((s2 ^\ N) . m)) - (f /. x0)).|| by A3, A7, FUNCT_2:109, XBOOLE_1:1, A10

.= ||.((f /. x0) - (f /. x0)).|| by A6, A10

.= ||.(0. T).|| by RLVECT_1:15

.= 0 by NORMSP_1:1 ;

hence ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p by A9; :: thesis: verum

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

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p )

assume A9: p > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p

reconsider n = 0 as Nat ;

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

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p )

assume n <= m ; :: thesis: ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p

A10: m in NAT by ORDINAL1:def 12;

||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| = ||.((f /. ((s2 ^\ N) . m)) - (f /. x0)).|| by A3, A7, FUNCT_2:109, XBOOLE_1:1, A10

.= ||.((f /. x0) - (f /. x0)).|| by A6, A10

.= ||.(0. T).|| by RLVECT_1:15

.= 0 by NORMSP_1:1 ;

hence ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p by A9; :: thesis: verum

A12: f /* (s2 ^\ N) = (f /* s2) ^\ N by A3, VALUED_0:27;

then A13: f /* s2 is convergent by A11, LOPBAN_3:10;

f /. x0 = lim ((f /* s2) ^\ N) by A8, A11, A12, NORMSP_1:def 7;

hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by A13, LOPBAN_3:9; :: thesis: verum

suppose A14:
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) )

( n <= m & s2 . m <> x0 ) ; :: thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )

defpred S_{1}[ 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 S_{2}[ Nat] means s2 . $1 <> x0;

ex m1 being Element of NAT st

( 0 <= m1 & s2 . m1 <> x0 ) by A14;

then A15: ex m being Nat st S_{2}[m]
;

consider M being Nat such that

A16: ( S_{2}[M] & ( for n being Nat st S_{2}[n] holds

M <= n ) ) from NAT_1:sch 5(A15);

reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

for x being Element of NAT ex y being Element of NAT st S_{1}[n,x,y]

A22: ( F . 0 = M9 & ( for n being Nat holds S_{1}[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 2(A19);

A23: rng F c= REAL by NUMBERS:19;

A24: rng F c= NAT ;

A25: dom F = NAT by FUNCT_2:def 1;

then reconsider F = F as Real_Sequence by A23, RELSET_1:4;

A28: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A4, LOPBAN_3:7, LOPBAN_3:8;

A29: for n being Element of NAT st s2 . n <> x0 holds

ex m being Element of NAT st F . m = n

then rng (s2 * F) c= dom f by A3;

then A45: ( f /* (s2 * F) is convergent & f /. x0 = lim (f /* (s2 * F)) ) by A2, A41, A28;

hence f /. x0 = lim (f /* s2) by A46, NORMSP_1:def 7; :: thesis: verum

end;( n < m & s2 . m <> x0 & ( for k being Element of NAT st n < k & s2 . k <> x0 holds

m <= k ) );

defpred S

ex m1 being Element of NAT st

( 0 <= m1 & s2 . m1 <> x0 ) by A14;

then A15: ex m being Nat st S

consider M being Nat such that

A16: ( S

M <= n ) ) from NAT_1:sch 5(A15);

reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

A17: now :: thesis: for n being Element of NAT ex m being Element of NAT st

( n < m & s2 . m <> x0 )

A19:
for n being Nat( 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

A18: ( n + 1 <= m & s2 . m <> x0 ) by A14;

take m = m; :: thesis: ( n < m & s2 . m <> x0 )

thus ( n < m & s2 . m <> x0 ) by A18, NAT_1:13; :: thesis: verum

end;( n < m & s2 . m <> x0 )

consider m being Element of NAT such that

A18: ( n + 1 <= m & s2 . m <> x0 ) by A14;

take m = m; :: thesis: ( n < m & s2 . m <> x0 )

thus ( n < m & s2 . m <> x0 ) by A18, NAT_1:13; :: thesis: verum

for x being Element of NAT ex y being Element of NAT st S

proof

consider F being sequence of NAT such that
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S_{1}[n,x,y]

let x be Element of NAT ; :: thesis: ex y being Element of NAT st S_{1}[n,x,y]

defpred S_{3}[ Nat] means ( x < $1 & s2 . $1 <> x0 );

ex m being Element of NAT st S_{3}[m]
by A17;

then A20: ex m being Nat st S_{3}[m]
;

consider l being Nat such that

A21: ( S_{3}[l] & ( for k being Nat st S_{3}[k] holds

l <= k ) ) from NAT_1:sch 5(A20);

reconsider l = l as Element of NAT by ORDINAL1:def 12;

take l ; :: thesis: S_{1}[n,x,l]

thus S_{1}[n,x,l]
by A21; :: thesis: verum

end;let x be Element of NAT ; :: thesis: ex y being Element of NAT st S

defpred S

ex m being Element of NAT st S

then A20: ex m being Nat st S

consider l being Nat such that

A21: ( S

l <= k ) ) from NAT_1:sch 5(A20);

reconsider l = l as Element of NAT by ORDINAL1:def 12;

take l ; :: thesis: S

thus S

A22: ( F . 0 = M9 & ( for n being Nat holds S

A23: rng F c= REAL by NUMBERS:19;

A24: rng F c= NAT ;

A25: dom F = NAT by FUNCT_2:def 1;

then reconsider F = F as Real_Sequence by A23, RELSET_1:4;

A26: 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 A25, FUNCT_1:def 3;

hence F . n is Element of NAT by A24; :: thesis: verum

end;F . n in rng F by A25, FUNCT_1:def 3;

hence F . n is Element of NAT by A24; :: thesis: verum

now :: thesis: for n being Nat holds F . n < F . (n + 1)

then reconsider F = F as V43() sequence of NAT by SEQM_3:def 6;let n be Nat; :: thesis: F . n < F . (n + 1)

A27: n in NAT by ORDINAL1:def 12;

( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A26, A27;

hence F . n < F . (n + 1) by A22; :: thesis: verum

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

( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A26, A27;

hence F . n < F . (n + 1) by A22; :: thesis: verum

A28: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A4, LOPBAN_3:7, LOPBAN_3:8;

A29: for n being Element of NAT st s2 . n <> x0 holds

ex m being Element of NAT st F . m = n

proof

A41:
for n being Nat holds (s2 * F) . n <> x0
defpred S_{3}[ Nat] means ( s2 . $1 <> x0 & ( for m being Element of NAT holds F . m <> $1 ) );

assume ex n being Element of NAT st S_{3}[n]
; :: thesis: contradiction

then A30: ex n being Nat st S_{3}[n]
;

consider M1 being Nat such that

A31: ( S_{3}[M1] & ( for n being Nat st S_{3}[n] holds

M1 <= n ) ) from NAT_1:sch 5(A30);

defpred S_{4}[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Element of NAT st F . m = $1 );

A32: ex n being Nat st S_{4}[n]
_{4}[n] holds

n <= M1 ;

consider MX being Nat such that

A34: ( S_{4}[MX] & ( for n being Nat st S_{4}[n] holds

n <= MX ) ) from NAT_1:sch 6(A33, A32);

A35: for k being Element of NAT st MX < k & k < M1 holds

s2 . k = x0

A38: F . m = MX by A34;

A39: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A22, A38;

M1 in NAT by ORDINAL1:def 12;

then A40: F . (m + 1) <= M1 by A22, A31, A34, A38;

end;assume ex n being Element of NAT st S

then A30: ex n being Nat st S

consider M1 being Nat such that

A31: ( S

M1 <= n ) ) from NAT_1:sch 5(A30);

defpred S

A32: ex n being Nat st S

proof

A33:
for n being Nat st S
take
M
; :: thesis: S_{4}[M]

( M <= M1 & M <> M1 ) by A16, A22, A31;

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 A16; :: thesis: ex m being Element of NAT st F . m = M

take 0 ; :: thesis: F . 0 = M

thus F . 0 = M by A22; :: thesis: verum

end;( M <= M1 & M <> M1 ) by A16, A22, A31;

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 A16; :: thesis: ex m being Element of NAT st F . m = M

take 0 ; :: thesis: F . 0 = M

thus F . 0 = M by A22; :: thesis: verum

n <= M1 ;

consider MX being Nat such that

A34: ( S

n <= MX ) ) from NAT_1:sch 6(A33, A32);

A35: for k being Element of NAT st MX < k & k < M1 holds

s2 . k = x0

proof

consider m being Element of NAT such that
given k being Element of NAT such that A36:
MX < k
and

A37: ( k < M1 & s2 . k <> x0 ) ; :: thesis: contradiction

end;A37: ( k < M1 & s2 . k <> x0 ) ; :: thesis: contradiction

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k )
;

end;

A38: F . m = MX by A34;

A39: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A22, A38;

M1 in NAT by ORDINAL1:def 12;

then A40: F . (m + 1) <= M1 by A22, A31, A34, A38;

now :: thesis: not F . (m + 1) <> M1

hence
contradiction
by A31; :: thesis: verumassume
F . (m + 1) <> M1
; :: thesis: contradiction

then F . (m + 1) < M1 by A40, XXREAL_0:1;

hence contradiction by A35, A39; :: thesis: verum

end;then F . (m + 1) < M1 by A40, XXREAL_0:1;

hence contradiction by A35, A39; :: thesis: verum

proof

A44:
rng (s2 * F) c= rng s2
by VALUED_0:21;
defpred S_{3}[ Nat] means (s2 * F) . $1 <> x0;

A42: for k being Nat st S_{3}[k] holds

S_{3}[k + 1]
_{3}[ 0 ]
by A16, A22, FUNCT_2:15;

thus for n being Nat holds S_{3}[n]
from NAT_1:sch 2(A43, A42); :: thesis: verum

end;A42: for k being Nat st S

S

proof

A43:
S
let k be Nat; :: thesis: ( S_{3}[k] implies S_{3}[k + 1] )

assume (s2 * F) . k <> x0 ; :: thesis: S_{3}[k + 1]

S_{1}[k,F . k,F . (k + 1)]
by A22;

then s2 . (F . (k + 1)) <> x0 ;

hence S_{3}[k + 1]
by FUNCT_2:15; :: thesis: verum

end;assume (s2 * F) . k <> x0 ; :: thesis: S

S

then s2 . (F . (k + 1)) <> x0 ;

hence S

thus for n being Nat holds S

then rng (s2 * F) c= dom f by A3;

then A45: ( f /* (s2 * F) is convergent & f /. x0 = lim (f /* (s2 * F)) ) by A2, A41, A28;

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

ex k being Nat st

for m being Nat st k <= m holds

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

hence
f /* s2 is convergent
; :: thesis: f /. x0 = lim (f /* s2)ex k being Nat st

for m being Nat st k <= m holds

||.(((f /* s2) . 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 /* s2) . m) - (f /. x0)).|| < p )

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

for m being Nat st k <= m holds

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

then consider n being Nat such that

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

||.(((f /* (s2 * F)) . m) - (f /. x0)).|| < p by A45, NORMSP_1:def 7;

reconsider k = F . n as Nat ;

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

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

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

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

A50: m in NAT by ORDINAL1:def 12;

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

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

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

for m being Nat st k <= m holds

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

then consider n being Nat such that

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

||.(((f /* (s2 * F)) . m) - (f /. x0)).|| < p by A45, NORMSP_1:def 7;

reconsider k = F . n as Nat ;

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

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

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

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

A50: m in NAT by ORDINAL1:def 12;

now :: thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < pend;

hence
||.(((f /* s2) . m) - (f /. x0)).|| < p
; :: thesis: verumper cases
( s2 . m = x0 or s2 . m <> x0 )
;

end;

suppose A51:
s2 . m = x0
; :: thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < p

||.(((f /* s2) . m) - (f /. x0)).|| =
||.((f /. (s2 . m)) - (f /. x0)).||
by A3, FUNCT_2:109, A50

.= ||.(0. T).|| by A51, RLVECT_1:15

.= 0 by NORMSP_1:1 ;

hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A47; :: thesis: verum

end;.= ||.(0. T).|| by A51, RLVECT_1:15

.= 0 by NORMSP_1:1 ;

hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A47; :: thesis: verum

suppose
s2 . m <> x0
; :: thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < p

then consider l being Element of NAT such that

A52: m = F . l by A29, A50;

n <= l by A49, A52, SEQM_3:1;

then ||.(((f /* (s2 * F)) . l) - (f /. x0)).|| < p by A48;

then ||.((f /. ((s2 * F) . l)) - (f /. x0)).|| < p by A3, A44, FUNCT_2:109, XBOOLE_1:1;

then ||.((f /. (s2 . m)) - (f /. x0)).|| < p by A52, FUNCT_2:15;

hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A3, FUNCT_2:109, A50; :: thesis: verum

end;A52: m = F . l by A29, A50;

n <= l by A49, A52, SEQM_3:1;

then ||.(((f /* (s2 * F)) . l) - (f /. x0)).|| < p by A48;

then ||.((f /. ((s2 * F) . l)) - (f /. x0)).|| < p by A3, A44, FUNCT_2:109, XBOOLE_1:1;

then ||.((f /. (s2 . m)) - (f /. x0)).|| < p by A52, FUNCT_2:15;

hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A3, FUNCT_2:109, A50; :: thesis: verum

hence f /. x0 = lim (f /* s2) by A46, NORMSP_1:def 7; :: thesis: verum