let n be non zero Element of NAT ; :: thesis: for R being PartFunc of REAL,(REAL-NS n) st R is total holds

( R is RestFunc-like iff for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

let R be PartFunc of REAL,(REAL-NS n); :: thesis: ( R is total implies ( R is RestFunc-like iff for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) ) )

assume A1: R is total ; :: thesis: ( R is RestFunc-like iff for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) ) by A2; :: thesis: verum

( R is RestFunc-like iff for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

let R be PartFunc of REAL,(REAL-NS n); :: thesis: ( R is total implies ( R is RestFunc-like iff for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) ) )

assume A1: R is total ; :: thesis: ( R is RestFunc-like iff for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

A2: now :: thesis: ( R is RestFunc-like & ex r being Real st

( r > 0 & ( for d being Real st d > 0 holds

ex z being Real st

( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ) ) implies for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

( r > 0 & ( for d being Real st d > 0 holds

ex z being Real st

( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ) ) implies for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

assume A3:
R is RestFunc-like
; :: thesis: ( ex r being Real st

( r > 0 & ( for d being Real st d > 0 holds

ex z being Real st

( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ) ) implies for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

given r being Real such that A4: r > 0 and

A5: for d being Real st d > 0 holds

ex z being Real st

( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ; :: thesis: for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) )

defpred S_{1}[ Nat, Real] means ( $2 <> 0 & |.$2.| < 1 / ($1 + 1) & not (|.$2.| ") * ||.(R /. $2).|| < r );

A6: for n being Element of NAT ex z being Element of REAL st S_{1}[n,z]

A8: for n being Element of NAT holds S_{1}[n,s . n]
from FUNCT_2:sch 3(A6);

A9: for n being Nat holds S_{1}[n,s . n]

then A16: lim s = 0 by A10, SEQ_2:def 7;

s is non-zero by A9, SEQ_1:5;

then reconsider s = s as non-zero 0 -convergent Real_Sequence by A15, A16, FDIFF_1:def 1;

( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) ) by A3, NDIFF_3:def 1;

then consider n0 being Nat such that

A17: for m being Nat st n0 <= m holds

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r by A4, NORMSP_1:def 7;

A18: ||.((((s ") (#) (R /* s)) . n0) - (0. (REAL-NS n))).|| < r by A17;

A19: ||.(((s . n0) ") * (R /. (s . n0))).|| = |.((s . n0) ").| * ||.(R /. (s . n0)).|| by NORMSP_1:def 1

.= (|.(s . n0).| ") * ||.(R /. (s . n0)).|| by COMPLEX1:66 ;

dom R = REAL by A1, PARTFUN1:def 2;

then A20: rng s c= dom R ;

A21: n0 in NAT by ORDINAL1:def 12;

||.((((s ") (#) (R /* s)) . n0) - (0. (REAL-NS n))).|| = ||.(((s ") (#) (R /* s)) . n0).|| by RLVECT_1:13

.= ||.(((s ") . n0) * ((R /* s) . n0)).|| by NDIFF_1:def 2

.= ||.(((s . n0) ") * ((R /* s) . n0)).|| by VALUED_1:10

.= ||.(((s . n0) ") * (R /. (s . n0))).|| by A20, A21, FUNCT_2:109 ;

hence for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) by A9, A18, A19; :: thesis: verum

end;( r > 0 & ( for d being Real st d > 0 holds

ex z being Real st

( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ) ) implies for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

given r being Real such that A4: r > 0 and

A5: for d being Real st d > 0 holds

ex z being Real st

( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ; :: thesis: for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) )

defpred S

A6: for n being Element of NAT ex z being Element of REAL st S

proof

consider s being Real_Sequence such that
let n be Element of NAT ; :: thesis: ex z being Element of REAL st S_{1}[n,z]

consider z being Real such that

A7: ( z <> 0 & |.z.| < 1 / (n + 1) & not (|.z.| ") * ||.(R /. z).|| < r ) by A5;

reconsider z = z as Element of REAL by XREAL_0:def 1;

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

( z <> 0 & |.z.| < 1 / (n + 1) & not (|.z.| ") * ||.(R /. z).|| < r ) by A7;

then S_{1}[n,z]
;

hence S_{1}[n,z]
; :: thesis: verum

end;consider z being Real such that

A7: ( z <> 0 & |.z.| < 1 / (n + 1) & not (|.z.| ") * ||.(R /. z).|| < r ) by A5;

reconsider z = z as Element of REAL by XREAL_0:def 1;

take z ; :: thesis: S

( z <> 0 & |.z.| < 1 / (n + 1) & not (|.z.| ") * ||.(R /. z).|| < r ) by A7;

then S

hence S

A8: for n being Element of NAT holds S

A9: for n being Nat holds S

proof

let n be Nat; :: thesis: S_{1}[n,s . n]

n in NAT by ORDINAL1:def 12;

hence S_{1}[n,s . n]
by A8; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence S

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

ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - 0).| < p

A15:
s is convergent
by A10, SEQ_2:def 6;ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - 0).| < p

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

for m being Nat st n <= m holds

|.((s . m) - 0).| < p )

assume A11: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - 0).| < p

consider n being Nat such that

A12: p " < n by SEQ_4:3;

reconsider q0 = 0 , q1 = 1 as Real ;

(p ") + q0 < n + q1 by A12, XREAL_1:8;

then A13: 1 / (n + 1) < 1 / (p ") by A11, XREAL_1:76;

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

|.((s . m) - 0).| < p

let m be Nat; :: thesis: ( n <= m implies |.((s . m) - 0).| < p )

assume n <= m ; :: thesis: |.((s . m) - 0).| < p

then A14: n + 1 <= m + 1 by XREAL_1:6;

1 / (m + 1) <= 1 / (n + 1) by A14, XREAL_1:118;

then |.((s . m) - 0).| < 1 / (n + 1) by A9, XXREAL_0:2;

hence |.((s . m) - 0).| < p by A13, XXREAL_0:2; :: thesis: verum

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

|.((s . m) - 0).| < p )

assume A11: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - 0).| < p

consider n being Nat such that

A12: p " < n by SEQ_4:3;

reconsider q0 = 0 , q1 = 1 as Real ;

(p ") + q0 < n + q1 by A12, XREAL_1:8;

then A13: 1 / (n + 1) < 1 / (p ") by A11, XREAL_1:76;

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

|.((s . m) - 0).| < p

let m be Nat; :: thesis: ( n <= m implies |.((s . m) - 0).| < p )

assume n <= m ; :: thesis: |.((s . m) - 0).| < p

then A14: n + 1 <= m + 1 by XREAL_1:6;

1 / (m + 1) <= 1 / (n + 1) by A14, XREAL_1:118;

then |.((s . m) - 0).| < 1 / (n + 1) by A9, XXREAL_0:2;

hence |.((s . m) - 0).| < p by A13, XXREAL_0:2; :: thesis: verum

then A16: lim s = 0 by A10, SEQ_2:def 7;

s is non-zero by A9, SEQ_1:5;

then reconsider s = s as non-zero 0 -convergent Real_Sequence by A15, A16, FDIFF_1:def 1;

( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) ) by A3, NDIFF_3:def 1;

then consider n0 being Nat such that

A17: for m being Nat st n0 <= m holds

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r by A4, NORMSP_1:def 7;

A18: ||.((((s ") (#) (R /* s)) . n0) - (0. (REAL-NS n))).|| < r by A17;

A19: ||.(((s . n0) ") * (R /. (s . n0))).|| = |.((s . n0) ").| * ||.(R /. (s . n0)).|| by NORMSP_1:def 1

.= (|.(s . n0).| ") * ||.(R /. (s . n0)).|| by COMPLEX1:66 ;

dom R = REAL by A1, PARTFUN1:def 2;

then A20: rng s c= dom R ;

A21: n0 in NAT by ORDINAL1:def 12;

||.((((s ") (#) (R /* s)) . n0) - (0. (REAL-NS n))).|| = ||.(((s ") (#) (R /* s)) . n0).|| by RLVECT_1:13

.= ||.(((s ") . n0) * ((R /* s) . n0)).|| by NDIFF_1:def 2

.= ||.(((s . n0) ") * ((R /* s) . n0)).|| by VALUED_1:10

.= ||.(((s . n0) ") * (R /. (s . n0))).|| by A20, A21, FUNCT_2:109 ;

hence for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) by A9, A18, A19; :: thesis: verum

now :: thesis: ( ( for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) ) implies R is RestFunc-like )

hence
( R is RestFunc-like iff for r being Real st r > 0 holds ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) ) implies R is RestFunc-like )

assume A22:
for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) ; :: thesis: R is RestFunc-like

end;ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) ; :: thesis: R is RestFunc-like

now :: thesis: for s being non-zero 0 -convergent Real_Sequence holds

( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) )

hence
R is RestFunc-like
by A1, NDIFF_3:def 1; :: thesis: verum( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) )

let s be non-zero 0 -convergent Real_Sequence; :: thesis: ( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) )

A23: ( s is convergent & lim s = 0 ) ;

hence lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) by A24, NORMSP_1:def 7; :: thesis: verum

end;A23: ( s is convergent & lim s = 0 ) ;

A24: now :: thesis: for r being Real st r > 0 holds

ex n0 being Nat st

for m being Nat st n0 <= m holds

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r

hence
(s ") (#) (R /* s) is convergent
by NORMSP_1:def 6; :: thesis: lim ((s ") (#) (R /* s)) = 0. (REAL-NS n)ex n0 being Nat st

for m being Nat st n0 <= m holds

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r

let r be Real; :: thesis: ( r > 0 implies ex n0 being Nat st

for m being Nat st n0 <= m holds

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r )

assume r > 0 ; :: thesis: ex n0 being Nat st

for m being Nat st n0 <= m holds

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r

then consider d being Real such that

A25: d > 0 and

A26: for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r by A22;

consider n0 being Nat such that

A27: for m being Nat st n0 <= m holds

|.((s . m) - 0).| < d by A23, A25, SEQ_2:def 7;

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

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r

thus for m being Nat st n0 <= m holds

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r :: thesis: verum

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

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r )

assume r > 0 ; :: thesis: ex n0 being Nat st

for m being Nat st n0 <= m holds

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r

then consider d being Real such that

A25: d > 0 and

A26: for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r by A22;

consider n0 being Nat such that

A27: for m being Nat st n0 <= m holds

|.((s . m) - 0).| < d by A23, A25, SEQ_2:def 7;

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

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r

thus for m being Nat st n0 <= m holds

||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r :: thesis: verum

proof

dom R = REAL
by A1, PARTFUN1:def 2;

then A28: rng s c= dom R ;

let m be Nat; :: thesis: ( n0 <= m implies ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r )

assume n0 <= m ; :: thesis: ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r

then A29: |.((s . m) - 0).| < d by A27;

A30: s . m <> 0 by SEQ_1:5;

A31: m in NAT by ORDINAL1:def 12;

(|.(s . m).| ") * ||.(R /. (s . m)).|| = |.((s . m) ").| * ||.(R /. (s . m)).|| by COMPLEX1:66

.= ||.(((s . m) ") * (R /. (s . m))).|| by NORMSP_1:def 1

.= ||.(((s . m) ") * ((R /* s) . m)).|| by A28, A31, FUNCT_2:109

.= ||.(((s ") . m) * ((R /* s) . m)).|| by VALUED_1:10

.= ||.(((s ") (#) (R /* s)) . m).|| by NDIFF_1:def 2

.= ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| by RLVECT_1:13 ;

hence ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r by A26, A29, A30; :: thesis: verum

end;then A28: rng s c= dom R ;

let m be Nat; :: thesis: ( n0 <= m implies ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r )

assume n0 <= m ; :: thesis: ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r

then A29: |.((s . m) - 0).| < d by A27;

A30: s . m <> 0 by SEQ_1:5;

A31: m in NAT by ORDINAL1:def 12;

(|.(s . m).| ") * ||.(R /. (s . m)).|| = |.((s . m) ").| * ||.(R /. (s . m)).|| by COMPLEX1:66

.= ||.(((s . m) ") * (R /. (s . m))).|| by NORMSP_1:def 1

.= ||.(((s . m) ") * ((R /* s) . m)).|| by A28, A31, FUNCT_2:109

.= ||.(((s ") . m) * ((R /* s) . m)).|| by VALUED_1:10

.= ||.(((s ") (#) (R /* s)) . m).|| by NDIFF_1:def 2

.= ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| by RLVECT_1:13 ;

hence ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r by A26, A29, A30; :: thesis: verum

hence lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) by A24, NORMSP_1:def 7; :: thesis: verum

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) ) by A2; :: thesis: verum