let S, T be RealNormSpace; :: thesis: for R being RestFunc of S,T

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

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

let R be RestFunc of S,T; :: thesis: for s being 0. S -convergent sequence of S st s is non-zero holds

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

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

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

A2: (||.s.|| ") (#) (R /* s) is convergent by Def5, A1;

A5: s is convergent by Def4;

then A6: ||.s.|| is convergent by LOPBAN_1:41;

lim s = 0. S by Def4;

then lim ||.s.|| = ||.(0. S).|| by A5, LOPBAN_1:41;

then A7: lim ||.s.|| = 0 by NORMSP_1:1;

lim ((||.s.|| ") (#) (R /* s)) = 0. T by Def5, A1;

then lim (R /* s) = 0 * (0. T) by A5, A4, A2, A7, Th14, LOPBAN_1:41;

hence ( R /* s is convergent & lim (R /* s) = 0. T ) by A4, A2, A6, Th13, RLVECT_1:10; :: thesis: verum

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

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

let R be RestFunc of S,T; :: thesis: for s being 0. S -convergent sequence of S st s is non-zero holds

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

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

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

A2: (||.s.|| ") (#) (R /* s) is convergent by Def5, A1;

now :: thesis: for n being Element of NAT holds (||.s.|| (#) ((||.s.|| ") (#) (R /* s))) . n = (R /* s) . n

then A4:
||.s.|| (#) ((||.s.|| ") (#) (R /* s)) = R /* s
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (||.s.|| (#) ((||.s.|| ") (#) (R /* s))) . n = (R /* s) . n

s . n <> 0. S by Th7, A1;

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

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

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

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

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

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

.= (||.(s . n).|| * (||.(s . n).|| ")) * ((R /* s) . n) by RLVECT_1:def 7

.= 1 * ((R /* s) . n) by A3, XCMPLX_0:def 7

.= (R /* s) . n by RLVECT_1:def 8 ; :: thesis: verum

end;s . n <> 0. S by Th7, A1;

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

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

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

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

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

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

.= (||.(s . n).|| * (||.(s . n).|| ")) * ((R /* s) . n) by RLVECT_1:def 7

.= 1 * ((R /* s) . n) by A3, XCMPLX_0:def 7

.= (R /* s) . n by RLVECT_1:def 8 ; :: thesis: verum

A5: s is convergent by Def4;

then A6: ||.s.|| is convergent by LOPBAN_1:41;

lim s = 0. S by Def4;

then lim ||.s.|| = ||.(0. S).|| by A5, LOPBAN_1:41;

then A7: lim ||.s.|| = 0 by NORMSP_1:1;

lim ((||.s.|| ") (#) (R /* s)) = 0. T by Def5, A1;

then lim (R /* s) = 0 * (0. T) by A5, A4, A2, A7, Th14, LOPBAN_1:41;

hence ( R /* s is convergent & lim (R /* s) = 0. T ) by A4, A2, A6, Th13, RLVECT_1:10; :: thesis: verum