let r be Real; :: thesis: for R being RestFunc holds r (#) R is RestFunc
let R be RestFunc; :: thesis: r (#) R is RestFunc
A1: R is total by Def2;

now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((r (#) R) /* h) is convergent & lim ((h ") (#) ((r (#) R) /* h)) = 0 )

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((r (#) R) /* h) is convergent & lim ((h ") (#) ((r (#) R) /* h)) = 0 )
A2: (h ") (#) ((r (#) R) /* h) = (h ") (#) (r (#) (R /* h)) by A1, RFUNCT_2:14
.= r (#) ((h ") (#) (R /* h)) by SEQ_1:19 ;
A3: (h ") (#) (R /* h) is convergent by Def2;
hence (h ") (#) ((r (#) R) /* h) is convergent by A2; :: thesis: lim ((h ") (#) ((r (#) R) /* h)) = 0
lim ((h ") (#) (R /* h)) = 0 by Def2;
hence lim ((h ") (#) ((r (#) R) /* h)) = r * 0 by A3, A2, SEQ_2:8
.= 0 ;
:: thesis: verum

end;

hence r (#) R is RestFunc by A1, Def2; :: thesis: verum