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;

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, 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;

then A4: ||.s.|| (#) ((||.s.|| ") (#) (R /* s)) = R /* s by FUNCT_2:63;
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