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 is non-zero by Def4;
A2: ( s is convergent & lim s = 0. S ) by Def4;

now

let n be Element of NAT ; :: thesis: (||.s.|| (#) ((||.s.|| " ) (#) (R /* s))) . n = (R /* s) . n
s . n <> 0. S by A1, Th7;
then A3: ||.(s . n).|| <> 0 by NORMSP_1:def 2;
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_1:def 10
.= ||.(s . n).|| * (((||.s.|| . n) " ) * ((R /* s) . n)) by VALUED_1:10
.= ||.(s . n).|| * ((||.(s . n).|| " ) * ((R /* s) . n)) by NORMSP_1:def 10
.= (||.(s . n).|| * (||.(s . n).|| " )) * ((R /* s) . n) by RLVECT_1:def 9
.= 1 * ((R /* s) . n) by A3, XCMPLX_0:def 7
.= (R /* s) . n by RLVECT_1:def 9 ; :: thesis: verum

end;

then A4: ||.s.|| (#) ((||.s.|| " ) (#) (R /* s)) = R /* s by FUNCT_2:113;
A5: ( (||.s.|| " ) (#) (R /* s) is convergent & lim ((||.s.|| " ) (#) (R /* s)) = 0. T ) by Def5;
( ||.s.|| is convergent & lim ||.s.|| = ||.(0. S).|| ) by A2, LOPBAN_1:47;
then ( ||.s.|| is convergent & lim ||.s.|| = 0 ) by NORMSP_1:5;
then ( R /* s is convergent & lim (R /* s) = 0 * (0. T) ) by A4, A5, Th13, Th14;
hence ( R /* s is convergent & lim (R /* s) = 0. T ) by RLVECT_1:23; :: thesis: verum