let F be RealNormSpace; :: thesis: for r being Real
for R being RestFunc of F holds r (#) R is RestFunc of F
let r be Real; :: thesis: for R being RestFunc of F holds r (#) R is RestFunc of F
let R be RestFunc of F; :: thesis: r (#) R is RestFunc of F
A1: R is total by Def1;
then A2: r (#) R is total by VFUNCT_1:34;
now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((r (#) R) /* h) is convergent & lim ((h ") (#) ((r (#) R) /* h)) = 0. F )
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((r (#) R) /* h) is convergent & lim ((h ") (#) ((r (#) R) /* h)) = 0. F )
dom R = REAL by A1, FUNCT_2:def 1;
then rng h c= dom R ;
then A3: (h ") (#) ((r (#) R) /* h) = (h ") (#) (r * (R /* h)) by NFCONT_3:4
.= r * ((h ") (#) (R /* h)) by NDIFF_1:10 ;
A4: (h ") (#) (R /* h) is convergent by Def1;
hence (h ") (#) ((r (#) R) /* h) is convergent by A3, NORMSP_1:22; :: thesis: lim ((h ") (#) ((r (#) R) /* h)) = 0. F
lim ((h ") (#) (R /* h)) = 0. F by Def1;
hence lim ((h ") (#) ((r (#) R) /* h)) = r * (0. F) by A4, A3, NORMSP_1:28
.= 0. F by RLVECT_1:10 ;
:: thesis: verum
end;
hence r (#) R is RestFunc of F by A2, Def1; :: thesis: verum