let T, S be non trivial RealNormSpace; :: thesis: for r being Real
for R being REST of S,T holds r (#) R is REST of S,T
let r be Real; :: thesis: for R being REST of S,T holds r (#) R is REST of S,T
let R be REST of S,T; :: thesis: r (#) R is REST of S,T
A1: R is total by Def5;

A2: now

let h be convergent_to_0 sequence of S; :: thesis: ( (||.h.|| ") (#) ((r (#) R) /* h) is convergent & lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T )
A3: (||.h.|| ") (#) (R /* h) is convergent by Def5;
A4: (||.h.|| ") (#) ((r (#) R) /* h) = (||.h.|| ") (#) (r * (R /* h)) by A1, Th31
.= r * ((||.h.|| ") (#) (R /* h)) by Th10 ;
hence (||.h.|| ") (#) ((r (#) R) /* h) is convergent by A3, NORMSP_1:22; :: thesis: lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T
lim ((||.h.|| ") (#) (R /* h)) = 0. T by Def5;
hence lim ((||.h.|| ") (#) ((r (#) R) /* h)) = r * (0. T) by A3, A4, NORMSP_1:28
.= 0. T by RLVECT_1:10 ;
:: thesis: verum

end;

r (#) R is total by A1, VFUNCT_1:34;
hence r (#) R is REST of S,T by A2, Def5; :: thesis: verum