now

let h be convergent_to_0 Complex_Sequence; :: thesis: ( (h " ) (#) ((a (#) R) /* h) is convergent & lim ((h " ) (#) ((a (#) R) /* h)) = 0c )
A1: ( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0c ) by Def3;
A2: (h " ) (#) ((a (#) R) /* h) = (h " ) (#) (a (#) (R /* h)) by CFCONT_1:30
.= a (#) ((h " ) (#) (R /* h)) by COMSEQ_1:16 ;
hence (h " ) (#) ((a (#) R) /* h) is convergent by A1; :: thesis: lim ((h " ) (#) ((a (#) R) /* h)) = 0c
thus lim ((h " ) (#) ((a (#) R) /* h)) = a * 0c by A1, A2, COMSEQ_2:18
.= 0c ; :: thesis: verum

end;

hence a (#) R is total REST-like PartFunc of COMPLEX , COMPLEX by Def3; :: thesis: verum