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
( (||.h.|| ") (#) ((r (#) R) /* h) is convergent & lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T )
let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( (||.h.|| ") (#) ((r (#) R) /* h) is convergent & lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T ) )
assume A3: h is non-zero ; :: thesis: ( (||.h.|| ") (#) ((r (#) R) /* h) is convergent & lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T )
A4: (||.h.|| ") (#) (R /* h) is convergent by A3, Def5;
A5: (||.h.|| ") (#) ((r (#) R) /* h) = (||.h.|| ") (#) (r * (R /* h)) by A1, Th26
.= r * ((||.h.|| ") (#) (R /* h)) by Th10 ;
hence (||.h.|| ") (#) ((r (#) R) /* h) is convergent by A4, NORMSP_1:22; :: thesis: lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T
lim ((||.h.|| ") (#) (R /* h)) = 0. T by A3, Def5;
hence lim ((||.h.|| ") (#) ((r (#) R) /* h)) = r * (0. T) by A4, A5, 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 RestFunc of S,T by A2, Def5; :: thesis: verum