let S, T be RealNormSpace; :: thesis: for R being PartFunc of S,T 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 Point of S st z <> 0. S & ||.z.|| < d holds

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

let R be PartFunc of S,T; :: 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 Point of S st z <> 0. S & ||.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 Point of S st z <> 0. S & ||.z.|| < d holds

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

ex d being Real st

( d > 0 & ( for z being Point of S st z <> 0. S & ||.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 Point of S st z <> 0. S & ||.z.|| < d holds

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

let R be PartFunc of S,T; :: 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 Point of S st z <> 0. S & ||.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 Point of S st z <> 0. S & ||.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 holds

( not d > 0 or ex z being Point of S st

( z <> 0. S & ||.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 Point of S st z <> 0. S & ||.z.|| < d holds

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

( r > 0 & ( for d being Real holds

( not d > 0 or ex z being Point of S st

( z <> 0. S & ||.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 Point of S st z <> 0. S & ||.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 holds

( not d > 0 or ex z being Point of S st

( z <> 0. S & ||.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 Point of S st z <> 0. S & ||.z.|| < d holds

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

assume ex r being Real st

( r > 0 & ( for d being Real holds

( not d > 0 or ex z being Point of S st

( z <> 0. S & ||.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 Point of S st z <> 0. S & ||.z.|| < d holds

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

then consider r being Real such that

A4: r > 0 and

A5: for d being Real st d > 0 holds

ex z being Point of S st

( z <> 0. S & ||.z.|| < d & not (||.z.|| ") * ||.(R /. z).|| < r ) ;

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

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

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

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

then lim s = 0. S by A9, NORMSP_1:def 7;

then reconsider s = s as 0. S -convergent sequence of S by A15, Def4;

s is non-zero by A8, Th7;

then ( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T ) by A3;

then consider n being Nat such that

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

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

A17: n in NAT by ORDINAL1:def 12;

A18: ||.((((||.s.|| ") (#) (R /* s)) . n) - (0. T)).|| < r by A16;

s . n <> 0. S by A8;

then ||.(s . n).|| <> 0 by NORMSP_0:def 5;

then A19: ||.(s . n).|| > 0 by NORMSP_1:4;

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

.= (||.(s . n).|| ") * ||.(R /. (s . n)).|| by A19, ABSVALUE:def 1 ;

dom R = the carrier of S by A1, PARTFUN1:def 2;

then A21: rng s c= dom R ;

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

.= ||.(((||.s.|| ") . n) * ((R /* s) . n)).|| by Def2

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

.= ||.((||.(s . n).|| ") * ((R /* s) . n)).|| by NORMSP_0:def 4

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

hence for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds

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

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

( not d > 0 or ex z being Point of S st

( z <> 0. S & ||.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 Point of S st z <> 0. S & ||.z.|| < d holds

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

assume ex r being Real st

( r > 0 & ( for d being Real holds

( not d > 0 or ex z being Point of S st

( z <> 0. S & ||.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 Point of S st z <> 0. S & ||.z.|| < d holds

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

then consider r being Real such that

A4: r > 0 and

A5: for d being Real st d > 0 holds

ex z being Point of S st

( z <> 0. S & ||.z.|| < d & not (||.z.|| ") * ||.(R /. z).|| < r ) ;

defpred S

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

proof

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

0 < 1 * ((n + 1) ") ;

then 0 < 1 / (n + 1) by XCMPLX_0:def 9;

hence ex z being Point of S st S_{1}[n,z]
by A5; :: thesis: verum

end;0 < 1 * ((n + 1) ") ;

then 0 < 1 / (n + 1) by XCMPLX_0:def 9;

hence ex z being Point of S st S

A7: for n being Element of NAT holds S

A8: 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 A7; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence S

A9: 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. S)).|| < p

then A15:
s is convergent
;ex n being Nat st

for m being Nat st n <= m holds

||.((s . m) - (0. S)).|| < 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. S)).|| < p )

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

for m being Nat st n <= m holds

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

consider n being Nat such that

A11: p " < n by SEQ_4:3;

(p ") + 0 < n + 1 by A11, XREAL_1:8;

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

then A12: 1 / (n + 1) < p by XCMPLX_1:216;

reconsider n = n as Nat ;

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

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

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

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

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

||.(s . m).|| < 1 / (m + 1) by A8;

then A14: ||.((s . m) - (0. S)).|| < 1 / (m + 1) by RLVECT_1:13;

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

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

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

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

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

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

for m being Nat st n <= m holds

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

consider n being Nat such that

A11: p " < n by SEQ_4:3;

(p ") + 0 < n + 1 by A11, XREAL_1:8;

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

then A12: 1 / (n + 1) < p by XCMPLX_1:216;

reconsider n = n as Nat ;

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

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

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

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

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

||.(s . m).|| < 1 / (m + 1) by A8;

then A14: ||.((s . m) - (0. S)).|| < 1 / (m + 1) by RLVECT_1:13;

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

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

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

then lim s = 0. S by A9, NORMSP_1:def 7;

then reconsider s = s as 0. S -convergent sequence of S by A15, Def4;

s is non-zero by A8, Th7;

then ( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T ) by A3;

then consider n being Nat such that

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

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

A17: n in NAT by ORDINAL1:def 12;

A18: ||.((((||.s.|| ") (#) (R /* s)) . n) - (0. T)).|| < r by A16;

s . n <> 0. S by A8;

then ||.(s . n).|| <> 0 by NORMSP_0:def 5;

then A19: ||.(s . n).|| > 0 by NORMSP_1:4;

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

.= (||.(s . n).|| ") * ||.(R /. (s . n)).|| by A19, ABSVALUE:def 1 ;

dom R = the carrier of S by A1, PARTFUN1:def 2;

then A21: rng s c= dom R ;

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

.= ||.(((||.s.|| ") . n) * ((R /* s) . n)).|| by Def2

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

.= ||.((||.(s . n).|| ") * ((R /* s) . n)).|| by NORMSP_0:def 4

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

hence for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds

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

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

ex d being Real st

( d > 0 & ( for z being Point of S st z <> 0. S & ||.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 Point of S st z <> 0. S & ||.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 Point of S st z <> 0. S & ||.z.|| < d holds

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

end;ex d being Real st

( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds

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

now :: thesis: for s being 0. S -convergent sequence of S st s is non-zero holds

( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T )

hence
R is RestFunc-like
by A1; :: thesis: verum( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T )

let s be 0. S -convergent sequence of S; :: thesis: ( s is non-zero implies ( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T ) )

assume A23: s is non-zero ; :: thesis: ( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T )

A24: ( s is convergent & lim s = 0. S ) by Def4;

hence lim ((||.s.|| ") (#) (R /* s)) = 0. T by A25, NORMSP_1:def 7; :: thesis: verum

end;assume A23: s is non-zero ; :: thesis: ( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T )

A24: ( s is convergent & lim s = 0. S ) by Def4;

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

ex n being Nat st

for m being Nat st n <= m holds

||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r

hence
(||.s.|| ") (#) (R /* s) is convergent
; :: thesis: lim ((||.s.|| ") (#) (R /* s)) = 0. Tex n being Nat st

for m being Nat st n <= m holds

||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r

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

for m being Nat st n <= m holds

||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r )

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

for m being Nat st n <= m holds

||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r

then consider d being Real such that

A26: d > 0 and

A27: for z being Point of S st z <> 0. S & ||.z.|| < d holds

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

consider n being Nat such that

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

||.((s . m) - (0. S)).|| < d by A24, A26, NORMSP_1:def 7;

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

||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r

thus for m being Nat st n <= m holds

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

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

||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r )

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

for m being Nat st n <= m holds

||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r

then consider d being Real such that

A26: d > 0 and

A27: for z being Point of S st z <> 0. S & ||.z.|| < d holds

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

consider n being Nat such that

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

||.((s . m) - (0. S)).|| < d by A24, A26, NORMSP_1:def 7;

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

||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r

thus for m being Nat st n <= m holds

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

proof

dom R = the carrier of S
by A1, PARTFUN1:def 2;

then A29: rng s c= dom R ;

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

A30: m in NAT by ORDINAL1:def 12;

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

then ||.((s . m) - (0. S)).|| < d by A28;

then A31: ||.(s . m).|| < d by RLVECT_1:13;

A32: s . m <> 0. S by Th7, A23;

then ||.(s . m).|| <> 0 by NORMSP_0:def 5;

then ||.(s . m).|| > 0 by NORMSP_1:4;

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

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

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

.= ||.(((||.s.|| . m) ") * ((R /* s) . m)).|| by NORMSP_0:def 4

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

.= ||.(((||.s.|| ") (#) (R /* s)) . m).|| by Def2

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

hence ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r by A27, A31, A32; :: thesis: verum

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

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

A30: m in NAT by ORDINAL1:def 12;

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

then ||.((s . m) - (0. S)).|| < d by A28;

then A31: ||.(s . m).|| < d by RLVECT_1:13;

A32: s . m <> 0. S by Th7, A23;

then ||.(s . m).|| <> 0 by NORMSP_0:def 5;

then ||.(s . m).|| > 0 by NORMSP_1:4;

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

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

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

.= ||.(((||.s.|| . m) ") * ((R /* s) . m)).|| by NORMSP_0:def 4

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

.= ||.(((||.s.|| ") (#) (R /* s)) . m).|| by Def2

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

hence ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r by A27, A31, A32; :: thesis: verum

hence lim ((||.s.|| ") (#) (R /* s)) = 0. T by A25, NORMSP_1:def 7; :: thesis: verum

ex d being Real st

( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds

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