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:
thus x0 in dom f by A1; :: according to NFCONT_1:def 5 :: thesis: for b1 being Element of K16(K17(NAT, the carrier of S)) holds
( not rng b1 c= dom f or not b1 is convergent or not lim b1 = x0 or ( f /* b1 is convergent & f /. x0 = lim (f /* b1) ) )

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) )
per 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 ) )
;
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
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
let n be Element of NAT ; :: thesis: (s2 ^\ N) . n = x0
s2 . (n + N) = x0 by ;
hence (s2 ^\ N) . n = x0 by NAT_1:def 3; :: thesis: verum
end;
A7: rng (s2 ^\ N) c= rng s2 by VALUED_0:21;
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
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
.= ||.((f /. x0) - (f /. x0)).|| by
.= ||.(0. T).|| by RLVECT_1:15
.= 0 by NORMSP_1:1 ;
hence ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p by A9; :: thesis: verum
end;
then A11: f /* (s2 ^\ N) is convergent ;
A12: f /* (s2 ^\ N) = (f /* s2) ^\ N by ;
then A13: f /* s2 is convergent by ;
f /. x0 = lim ((f /* s2) ^\ N) by ;
hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by ; :: thesis: verum
end;
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) )
defpred S1[ 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[ 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 S2[m] ;
consider M being Nat such that
A16: ( S2[M] & ( for n being Nat st S2[n] holds
M <= n ) ) from 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 )
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 ; :: thesis: verum
end;
A19: for n being Nat
for x being Element of NAT ex y being Element of NAT st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S1[n,x,y]
let 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 A17;
then A20: ex m being Nat st S3[m] ;
consider l being Nat such that
A21: ( S3[l] & ( for k being Nat st S3[k] holds
l <= k ) ) from reconsider l = l as Element of NAT by ORDINAL1:def 12;
take l ; :: thesis: S1[n,x,l]
thus S1[n,x,l] by A21; :: thesis: verum
end;
consider F being sequence of NAT such that
A22: ( F . 0 = M9 & ( for n being Nat holds S1[n,F . n,F . (n + 1)] ) ) from 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 ;
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 ;
hence F . n is Element of NAT by A24; :: thesis: verum
end;
now :: thesis: for n being Nat holds F . n < F . (n + 1)
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 ;
hence F . n < F . (n + 1) by A22; :: thesis: verum
end;
then reconsider F = F as V43() sequence of NAT by SEQM_3:def 6;
A28: ( s2 * F is convergent & lim (s2 * F) = x0 ) by ;
A29: for n being Element of NAT st s2 . n <> x0 holds
ex m being Element of NAT st F . m = n
proof
defpred S3[ Nat] 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 A30: ex n being Nat st S3[n] ;
consider M1 being Nat such that
A31: ( S3[M1] & ( for n being Nat st S3[n] holds
M1 <= n ) ) from defpred S4[ Nat] means ( \$1 < M1 & s2 . \$1 <> x0 & ex m being Element of NAT st F . m = \$1 );
A32: ex n being Nat st S4[n]
proof
take M ; :: thesis: S4[M]
( M <= M1 & M <> M1 ) by ;
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;
A33: for n being Nat st S4[n] holds
n <= M1 ;
consider MX being Nat such that
A34: ( S4[MX] & ( for n being Nat st S4[n] holds
n <= MX ) ) from A35: for k being Element of NAT st MX < k & k < M1 holds
s2 . k = x0
proof
given k being Element of NAT such that A36: MX < k and
A37: ( k < M1 & s2 . k <> x0 ) ; :: thesis: contradiction
per cases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider m being Element of NAT such that
A38: F . m = MX by A34;
A39: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by ;
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
assume F . (m + 1) <> M1 ; :: thesis: contradiction
then F . (m + 1) < M1 by ;
hence contradiction by A35, A39; :: thesis: verum
end;
hence contradiction by A31; :: thesis: verum
end;
A41: for n being Nat holds (s2 * F) . n <> x0
proof
defpred S3[ Nat] means (s2 * F) . \$1 <> x0;
A42: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be 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 A22;
then s2 . (F . (k + 1)) <> x0 ;
hence S3[k + 1] by FUNCT_2:15; :: thesis: verum
end;
A43: S3[ 0 ] by ;
thus for n being Nat holds S3[n] from :: thesis: verum
end;
A44: rng (s2 * F) c= rng s2 by VALUED_0:21;
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
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 ;
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)).|| < p
per cases ( s2 . m = x0 or s2 . m <> x0 ) ;
suppose A51: s2 . m = x0 ; :: thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < p
||.(((f /* s2) . m) - (f /. x0)).|| = ||.((f /. (s2 . m)) - (f /. x0)).|| by
.= ||.(0. T).|| by
.= 0 by NORMSP_1:1 ;
hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A47; :: thesis: verum
end;
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 ;
n <= l by ;
then ||.(((f /* (s2 * F)) . l) - (f /. x0)).|| < p by A48;
then ||.((f /. ((s2 * F) . l)) - (f /. x0)).|| < p by ;
then ||.((f /. (s2 . m)) - (f /. x0)).|| < p by ;
hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by ; :: thesis: verum
end;
end;
end;
hence ||.(((f /* s2) . m) - (f /. x0)).|| < p ; :: thesis: verum
end;
hence f /* s2 is convergent ; :: thesis: f /. x0 = lim (f /* s2)
hence f /. x0 = lim (f /* s2) by ; :: thesis: verum
end;
end;
end;
hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) ; :: thesis: verum