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

now

let n be Element of NAT ; :: thesis: (||.s.|| (#) ((||.s.|| ") (#) (R /* s))) . n = (R /* s) . n
s . n <> 0. S by A2, Th7;
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;
then lim (R /* s) = 0 * (0. T) by A5, A4, A1, A7, Th14, LOPBAN_1:41;
hence ( R /* s is convergent & lim (R /* s) = 0. T ) by A4, A1, A6, Th13, RLVECT_1:10; :: thesis: verum