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

let h be non-zero 0 -convergent Complex_Sequence; :: thesis: ( (h ") (#) ((a (#) R) /* h) is convergent & lim ((h ") (#) ((a (#) R) /* h)) = 0c )
A1: (h ") (#) ((a (#) R) /* h) = (h ") (#) (a (#) (R /* h)) by CFCONT_1:15
.= a (#) ((h ") (#) (R /* h)) by COMSEQ_1:13 ;
A2: (h ") (#) (R /* h) is convergent by Def3;
hence (h ") (#) ((a (#) R) /* h) is convergent by A1; :: thesis: lim ((h ") (#) ((a (#) R) /* h)) = 0c
lim ((h ") (#) (R /* h)) = 0c by Def3;
hence lim ((h ") (#) ((a (#) R) /* h)) = a * 0c by A2, A1, COMSEQ_2:18
.= 0c ;
:: thesis: verum

end;

hence for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = a (#) R holds
( b₁ is total & b₁ is RestFunc-like ) ; :: thesis: verum