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

( f is_continuous_in x0 iff 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) ) )

let f be PartFunc of REAL,REAL; :: thesis: ( f is_continuous_in x0 iff 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) ) )

thus ( f is_continuous_in x0 implies 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: ( ( 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) ) ) implies f is_continuous_in x0 )

assume A1: 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: f is_continuous_in x0

let s2 be Real_Sequence; :: according to FCONT_1:def 1 :: thesis: ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) )

assume that

A2: rng s2 c= dom f and

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

( f is_continuous_in x0 iff 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) ) )

let f be PartFunc of REAL,REAL; :: thesis: ( f is_continuous_in x0 iff 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) ) )

thus ( f is_continuous_in x0 implies 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: ( ( 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) ) ) implies f is_continuous_in x0 )

assume A1: 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: f is_continuous_in x0

let s2 be Real_Sequence; :: according to FCONT_1:def 1 :: thesis: ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) )

assume that

A2: rng s2 c= dom f and

A3: ( 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

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

s2 . m = x0 ;

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

A7: rng (s2 ^\ N) c= rng s2 by VALUED_0:21;

then f . x0 = lim ((f /* s2) ^\ N) by A8, A6, SEQ_2:def 7;

hence ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) by A11, A6, SEQ_4:20, SEQ_4:21; :: thesis: verum

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

s2 . m = x0 ;

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

proof

A6:
f /* (s2 ^\ N) = (f /* s2) ^\ N
by A2, VALUED_0:27;
let n be Element of NAT ; :: thesis: (s2 ^\ N) . n = x0

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

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

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

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

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

then A11:
f /* (s2 ^\ N) is convergent
by SEQ_2:def 6;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 zz = 0 as Nat ;

take n = zz; :: 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;

then |.(((f /* (s2 ^\ N)) . m) - (f . x0)).| = |.((f . ((s2 ^\ N) . m)) - (f . x0)).| by A2, A7, FUNCT_2:108, XBOOLE_1:1

.= |.((f . x0) - (f . x0)).| by A5, A10

.= 0 by ABSVALUE:2 ;

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 zz = 0 as Nat ;

take n = zz; :: 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;

then |.(((f /* (s2 ^\ N)) . m) - (f . x0)).| = |.((f . ((s2 ^\ N) . m)) - (f . x0)).| by A2, A7, FUNCT_2:108, XBOOLE_1:1

.= |.((f . x0) - (f . x0)).| by A5, A10

.= 0 by ABSVALUE:2 ;

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

then f . x0 = lim ((f /* s2) ^\ N) by A8, A6, SEQ_2:def 7;

hence ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) by A11, A6, SEQ_4:20, SEQ_4:21; :: thesis: verum

suppose A12:
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}[ set ] means s2 . $1 <> x0;

ex m1 being Element of NAT st

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

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

consider M being Nat such that

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

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

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]

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

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

A22: rng F c= NAT ;

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

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

A25: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A3, SEQ_4:16, SEQ_4:17;

A26: 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 A2;

then A42: ( f /* (s2 * F) is convergent & f . x0 = lim (f /* (s2 * F)) ) by A1, A38, A25;

hence f . x0 = lim (f /* s2) by A43, SEQ_2: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 A12;

then A13: ex m being Nat st S

consider M being Nat such that

A14: ( S

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

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

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

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

A17:
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

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

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

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

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

consider m being Element of NAT such that

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

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

thus ( n < m & s2 . m <> x0 ) by A16, 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 A15;

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

consider l being Nat such that

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

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

take l ; :: thesis: ( l is Element of NAT & S_{1}[n,x,l] )

l in NAT by ORDINAL1:def 12;

hence ( l is Element of NAT & S_{1}[n,x,l] )
by A19; :: 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 A18: ex m being Nat st S

consider l being Nat such that

A19: ( S

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

take l ; :: thesis: ( l is Element of NAT & S

l in NAT by ORDINAL1:def 12;

hence ( l is Element of NAT & S

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

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

A22: rng F c= NAT ;

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

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

A24: 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 A23, FUNCT_1:def 3;

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

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

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

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

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

n in NAT by ORDINAL1:def 12;

then ( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A24;

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

end;n in NAT by ORDINAL1:def 12;

then ( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A24;

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

A25: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A3, SEQ_4:16, SEQ_4:17;

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

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

proof

A38:
for n being Nat holds (s2 * F) . n <> x0
defpred S_{3}[ set ] 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 A27: ex n being Nat st S_{3}[n]
;

consider M1 being Nat such that

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

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

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

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

n <= M1 ;

consider MX being Nat such that

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

n <= MX ) ) from NAT_1:sch 6(A30, A29);

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

s2 . k = x0

A35: F . m = MX by A31;

A36: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A20, A35;

M1 in NAT by ORDINAL1:def 12;

then A37: F . (m + 1) <= M1 by A20, A28, A31, A35;

end;assume ex n being Element of NAT st S

then A27: ex n being Nat st S

consider M1 being Nat such that

A28: ( S

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

defpred S

A29: ex n being Nat st S

proof

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

( M <= M1 & M <> M1 ) by A14, A20, A28;

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

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

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

end;( M <= M1 & M <> M1 ) by A14, A20, A28;

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

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

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

n <= M1 ;

consider MX being Nat such that

A31: ( S

n <= MX ) ) from NAT_1:sch 6(A30, A29);

A32: 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 A33:
MX < k
and

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

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

A35: F . m = MX by A31;

A36: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A20, A35;

M1 in NAT by ORDINAL1:def 12;

then A37: F . (m + 1) <= M1 by A20, A28, A31, A35;

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

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

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

hence contradiction by A32, A36; :: thesis: verum

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

hence contradiction by A32, A36; :: thesis: verum

proof

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

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

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

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

end;A39: for k being Nat st S

S

proof

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

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

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

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

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

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

S

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

hence S

thus for n being Nat holds S

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

then A42: ( f /* (s2 * F) is convergent & f . x0 = lim (f /* (s2 * F)) ) by A1, A38, A25;

A43: 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
by SEQ_2:def 6; :: 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 A44: 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

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

|.(((f /* (s2 * F)) . m) - (f . x0)).| < p by A42, SEQ_2: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 A46: k <= m ; :: thesis: |.(((f /* s2) . m) - (f . x0)).| < p

A47: m in NAT by ORDINAL1:def 12;

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

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

assume A44: 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

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

|.(((f /* (s2 * F)) . m) - (f . x0)).| < p by A42, SEQ_2: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 A46: k <= m ; :: thesis: |.(((f /* s2) . m) - (f . x0)).| < p

A47: 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
s2 . m = x0
; :: thesis: |.(((f /* s2) . m) - (f . x0)).| < p

then |.(((f /* s2) . m) - (f . x0)).| =
|.((f . x0) - (f . x0)).|
by A2, FUNCT_2:108, A47

.= 0 by ABSVALUE:2 ;

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

end;.= 0 by ABSVALUE:2 ;

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

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

then consider l being Element of NAT such that

A48: m = F . l by A26, A47;

n <= l by A46, A48, SEQM_3:1;

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

then |.((f . ((s2 * F) . l)) - (f . x0)).| < p by A2, A41, FUNCT_2:108, XBOOLE_1:1;

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

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

end;A48: m = F . l by A26, A47;

n <= l by A46, A48, SEQM_3:1;

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

then |.((f . ((s2 * F) . l)) - (f . x0)).| < p by A2, A41, FUNCT_2:108, XBOOLE_1:1;

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

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

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