let x0 be Real; :: thesis:
let S be RealNormSpace; :: thesis:
let f be PartFunc of REAL, the carrier of S; :: thesis:
thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for s1 being Real_Sequence 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:
assume A1: ( x0 in dom f & ( for s1 being Real_Sequence 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:
thus x0 in dom f by A1; :: according to NFCONT_3:def 1 :: thesis:
let s2 be Real_Sequence; :: thesis:
assume that
A2: rng s2 c= dom f and
A3: ( s2 is convergent & lim s2 = x0 ) ; :: thesis:

suppose ex n being Nat st
for m being Nat st n <= m holds
s2 . m = x0 ; :: thesis:

then consider N being Nat such that
A4: for m being Nat st N <= m holds
s2 . m = x0 ;
A5: f /* (s2 ^\ N) = (f /* s2) ^\ N by A2, VALUED_0:27;

let p be Real; :: thesis:
assume A7: p > 0 ; :: thesis:
reconsider n = 0 as Nat ;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
A8: s2 . (m + N) = x0 by A4, NAT_1:12;
A9: m in NAT by ORDINAL1:def 12;
rng (s2 ^\ N) c= rng s2 by VALUED_0:21;
then ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| = ||.((f /. ((s2 ^\ N) . m)) - (f /. x0)).|| by A2, FUNCT_2:109, XBOOLE_1:1, A9
.= ||.((f /. x0) - (f /. x0)).|| by A8, NAT_1:def 3
.= 0 by NORMSP_1:6 ;
hence ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p by A7; :: thesis:

end;

end;

defpred S₁[ Nat, set , set ] means for n, m being Nat st $2 = n & $3 = m holds
( n < m & s2 . m <> x0 & ( for k being Nat st n < k & s2 . k <> x0 holds
m <= k ) );
defpred S₂[ set ] means s2 . $1 <> x0;
ex m1 being Nat st
( 0 <= m1 & s2 . m1 <> x0 ) by A11;
then A12: ex m being Nat st S₂[m] ;
consider M being Nat such that
A13: ( S₂[M] & ( for n being Nat st S₂[n] holds
M <= n ) ) from NAT_1:sch 5(A12);
reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

let n be Nat; :: thesis:
consider m being Nat such that
A15: ( n + 1 <= m & s2 . m <> x0 ) by A11;
take m = m; :: thesis:
thus ( n < m & s2 . m <> x0 ) by A15, NAT_1:13; :: thesis:

end;

A16: for n being Nat
for x being Element of NAT ex y being Element of NAT st S₁[n,x,y]

let n be Nat; :: thesis:
let x be Element of NAT ; :: thesis:
defpred S₃[ Nat] means ( x < $1 & s2 . $1 <> x0 );
ex m being Nat st S₃[m] by A14;
then A17: ex m being Nat st S₃[m] ;
consider l being Nat such that
A18: ( S₃[l] & ( for k being Nat st S₃[k] holds
l <= k ) ) from NAT_1:sch 5(A17);
take l ; :: thesis:
l in NAT by ORDINAL1:def 12;
hence ( l is Element of NAT & S₁[n,x,l] ) by A18; :: thesis:

end;

consider F being sequence of NAT such that
A19: ( F . 0 = M9 & ( for n being Nat holds S₁[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A16);
( dom F = NAT & rng F c= REAL ) by FUNCT_2:def 1, XBOOLE_1:1, NUMBERS:19;
then reconsider F = F as Real_Sequence by RELSET_1:4;
for n being Nat holds F . n < F . (n + 1) by A19;
then reconsider F = F as increasing sequence of NAT by SEQM_3:def 6;
A20: for n being Nat st s2 . n <> x0 holds
ex m being Nat st F . m = n

defpred S₃[ set ] means ( s2 . $1 <> x0 & ( for m being Nat holds F . m <> $1 ) );
assume ex n being Nat st S₃[n] ; :: thesis:
then A21: ex n being Nat st S₃[n] ;
consider M1 being Nat such that
A22: ( S₃[M1] & ( for n being Nat st S₃[n] holds
M1 <= n ) ) from NAT_1:sch 5(A21);
reconsider M1 = M1 as Nat ;
defpred S₄[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Nat st F . m = $1 );
A23: ex n being Nat st S₄[n]

take M ; :: thesis:
( M <= M1 & M <> M1 ) by A13, A19, A22;
hence M < M1 by XXREAL_0:1; :: thesis:
thus s2 . M <> x0 by A13; :: thesis:
take 0 ; :: thesis:
thus F . 0 = M by A19; :: thesis:

end;

A24: for n being Nat st S₄[n] holds
n <= M1 ;
consider MX being Nat such that
A25: ( S₄[MX] & ( for n being Nat st S₄[n] holds
n <= MX ) ) from NAT_1:sch 6(A24, A23);
consider m being Nat such that
A26: F . m = MX by A25;
A27: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A19, A26;
( F . (m + 1) <> M1 & F . (m + 1) <= M1 ) by A19, A22, A25, A26;
then F . (m + 1) < M1 by XXREAL_0:1;
hence contradiction by A25, A27; :: thesis:

end;

defpred S₃[ Nat] means (s2 * F) . $1 <> x0;
A29: for k being Nat st S₃[k] holds
S₃[k + 1]

let k be Nat; :: thesis:
assume (s2 * F) . k <> x0 ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 12;
( F . k in NAT & F . (k + 1) in NAT ) ;
then s2 . (F . (k + 1)) <> x0 by A19;
hence S₃[k + 1] by FUNCT_2:15; :: thesis:

end;

end;

let p be Real; :: thesis:
assume A35: 0 < p ; :: thesis:
then consider n being Nat such that
A36: for m being Nat st n <= m holds
||.(((f /* (s2 * F)) . m) - (f /. x0)).|| < p by A33, NORMSP_1:def 7;
reconsider k = F . n as Nat ;
take k = k; :: thesis:
let m be Nat; :: thesis:
assume A37: k <= m ; :: thesis:
A38: m in NAT by ORDINAL1:def 12;

then ||.(((f /* s2) . m) - (f /. x0)).|| = ||.((f /. x0) - (f /. x0)).|| by A2, FUNCT_2:109, A38
.= 0 by NORMSP_1:6 ;
hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A35; :: thesis:

end;

then consider l being Nat such that
A39: m = F . l by A20;
A40: l in NAT by ORDINAL1:def 12;
n <= l by A37, A39, SEQM_3:1;
then ||.(((f /* (s2 * F)) . l) - (f /. x0)).|| < p by A36;
then ||.((f /. ((s2 * F) . l)) - (f /. x0)).|| < p by A2, A32, FUNCT_2:109, XBOOLE_1:1, A40;
then ||.((f /. (s2 . m)) - (f /. x0)).|| < p by A39, FUNCT_2:15, A40;
hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A2, FUNCT_2:109, A38; :: thesis:

end;

end;