let S, T be RealNormSpace; :: thesis: for r being Real
for R being RestFunc of S,T holds r (#) R is RestFunc of S,T

let r be Real; :: thesis: for R being RestFunc of S,T holds r (#) R is RestFunc of S,T
let R be RestFunc of S,T; :: thesis: r (#) R is RestFunc of S,T
A1: R is total by Def5;
A2: now :: thesis: for h being 0. S -convergent sequence of S st h is non-zero holds
( () (#) ((r (#) R) /* h) is convergent & lim (() (#) ((r (#) R) /* h)) = 0. T )
let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( () (#) ((r (#) R) /* h) is convergent & lim (() (#) ((r (#) R) /* h)) = 0. T ) )
assume A3: h is non-zero ; :: thesis: ( () (#) ((r (#) R) /* h) is convergent & lim (() (#) ((r (#) R) /* h)) = 0. T )
A4: (||.h.|| ") (#) (R /* h) is convergent by ;
A5: () (#) ((r (#) R) /* h) = () (#) (r * (R /* h)) by
.= r * (() (#) (R /* h)) by Th10 ;
hence (||.h.|| ") (#) ((r (#) R) /* h) is convergent by ; :: thesis: lim (() (#) ((r (#) R) /* h)) = 0. T
lim (() (#) (R /* h)) = 0. T by ;
hence lim (() (#) ((r (#) R) /* h)) = r * (0. T) by
.= 0. T by RLVECT_1:10 ;
:: thesis: verum
end;
r (#) R is total by ;
hence r (#) R is RestFunc of S,T by ; :: thesis: verum