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 ) ) )
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 ) ) )
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 S1[ 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 S1[n,z]
proof
let n be Element of NAT ; :: thesis: ex z being Point of S st S1[n,z]
0 < 1 * ((n + 1) ") ;
then 0 < 1 / (n + 1) by XCMPLX_0:def 9;
hence ex z being Point of S st S1[n,z] by A5; :: thesis: verum
end;
consider s being sequence of S such that
A7: for n being Element of NAT holds S1[n,s . n] from FUNCT_2:sch 3(A6);
A8: for n being Nat holds S1[n,s . n]
proof
let n be Nat; :: thesis: S1[n,s . n]
n in NAT by ORDINAL1:def 12;
hence S1[n,s . n] by A7; :: thesis: verum
end;
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
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;
then A15: s is convergent ;
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;
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 )
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
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 )
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;
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
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
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;
end;
hence (||.s.|| ") (#) (R /* s) is convergent ; :: thesis: lim ((||.s.|| ") (#) (R /* s)) = 0. T
hence lim ((||.s.|| ") (#) (R /* s)) = 0. T by A25, NORMSP_1:def 7; :: thesis: verum
end;
hence R is RestFunc-like by A1; :: thesis: verum
end;
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 ) ) ) by A2; :: thesis: verum