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 ;
now :: thesis: for n being Element of NAT holds ( (#) (() (#) (R /* s))) . n = (R /* s) . n
let n be Element of NAT ; :: thesis: ( (#) (() (#) (R /* s))) . n = (R /* s) . n
s . n <> 0. S by ;
then A3: ||.(s . n).|| <> 0 by NORMSP_0:def 5;
thus ( (#) (() (#) (R /* s))) . n = ( . n) * ((() (#) (R /* s)) . n) by Def2
.= ( . n) * ((() . n) * ((R /* s) . n)) by Def2
.= ||.(s . n).|| * ((() . n) * ((R /* s) . n)) by NORMSP_0:def 4
.= ||.(s . n).|| * ((( . 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
.= (R /* s) . n by RLVECT_1:def 8 ; :: thesis: verum
end;
then A4: ||.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 = ||.(0. S).|| by ;
then A7: lim = 0 by NORMSP_1:1;
lim (() (#) (R /* s)) = 0. T by ;
then lim (R /* s) = 0 * (0. T) by ;
hence ( R /* s is convergent & lim (R /* s) = 0. T ) by ; :: thesis: verum