let S, T be RealNormSpace; 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; 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; ( 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) ) ) ) )
; ( 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) )
; f is_continuous_in x0
thus
x0 in dom f
by A1; NFCONT_1:def 5 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; ( 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 )
; ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
now ( 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 A14:
for
n being
Element of
NAT ex
m being
Element of
NAT st
(
n <= m &
s2 . m <> x0 )
;
( 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 NAT_1:sch 5(A15);
reconsider M9 =
M as
Element of
NAT by ORDINAL1:def 12;
A19:
for
n being
Nat for
x being
Element of
NAT ex
y being
Element of
NAT st
S1[
n,
x,
y]
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 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;
then reconsider F =
F as
V43()
sequence of
NAT by SEQM_3:def 6;
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
A41:
for
n being
Nat holds
(s2 * F) . n <> x0
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;
hence
f /* s2 is
convergent
;
f /. x0 = lim (f /* s2)hence
f /. x0 = lim (f /* s2)
by A46, NORMSP_1:def 7;
verum end; end; end;
hence
( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
; verum