let S, T be RealNormSpace; for r being Real
for R being RestFunc of S,T holds r (#) R is RestFunc of S,T
let r be Real; for R being RestFunc of S,T holds r (#) R is RestFunc of S,T
let R be RestFunc of S,T; r (#) R is RestFunc of S,T
A1:
R is total
by Def5;
r (#) R is total
by A1, VFUNCT_1:34;
hence
r (#) R is RestFunc of S,T
by A2, Def5; verum