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

now

let h be convergent_to_0 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:33
.= r (#) ((h " ) (#) (R /* h)) by SEQ_1:27 ;
A3: (h " ) (#) (R /* h) is convergent by Def3;
hence (h " ) (#) ((r (#) R) /* h) is convergent by A2, SEQ_2:21; :: thesis: lim ((h " ) (#) ((r (#) R) /* h)) = 0
lim ((h " ) (#) (R /* h)) = 0 by Def3;
hence lim ((h " ) (#) ((r (#) R) /* h)) = r * 0 by A3, A2, SEQ_2:22
.= 0 ;
:: thesis: verum

end;

hence r (#) R is REST by A1, Def3; :: thesis: verum