let S, T be non trivial RealNormSpace; :: thesis: for R being RestFunc of S,T
for s being non-zero 0. S -convergent sequence of S holds
( R /* s is convergent & lim (R /* s) = 0. T )
let R be RestFunc of S,T; :: thesis: for s being non-zero 0. S -convergent sequence of S holds
( R /* s is convergent & lim (R /* s) = 0. T )
let s be non-zero 0. S -convergent sequence of S; :: thesis: ( R /* s is convergent & lim (R /* s) = 0. T )
A1: (||.s.|| ") (#) (R /* s) is convergent by Def5;

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

let n be Element of NAT ; :: thesis: (||.s.|| (#) ((||.s.|| ") (#) (R /* s))) . n = (R /* s) . n
s . n <> 0. S by Th7;
then A2: ||.(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 A2, XCMPLX_0:def 7
.= (R /* s) . n by RLVECT_1:def 8 ; :: thesis: verum

end;

then A3: ||.s.|| (#) ((||.s.|| ") (#) (R /* s)) = R /* s by FUNCT_2:63;
A4: s is convergent by Def4;
then A5: ||.s.|| is convergent by LOPBAN_1:41;
lim s = 0. S by Def4;
then lim ||.s.|| = ||.(0. S).|| by A4, LOPBAN_1:41;
then A6: lim ||.s.|| = 0 by NORMSP_1:1;
lim ((||.s.|| ") (#) (R /* s)) = 0. T by Def5;
then lim (R /* s) = 0 * (0. T) by A4, A3, A1, A6, Th14, LOPBAN_1:41;
hence ( R /* s is convergent & lim (R /* s) = 0. T ) by A3, A1, A5, Th13, RLVECT_1:10; :: thesis: verum