now

let h be convergent_to_0 Complex_Sequence; :: thesis: ( (h " ) (#) ((R1 (#) R2) /* h) is convergent & lim ((h " ) (#) ((R1 (#) R2) /* h)) = 0c )
A7: ( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0c ) by Def3;
A8: ( (h " ) (#) (R2 /* h) is convergent & lim ((h " ) (#) (R2 /* h)) = 0c ) by Def3;
A9: ( h is non-zero & h is convergent & lim h = 0c ) by Def1;
for seq being Complex_Sequence st seq is non-zero holds
seq " is non-zero

proof

let seq be Complex_Sequence; :: thesis: ( seq is non-zero implies seq " is non-zero )
assume that
A10: seq is non-zero and
A11: not seq " is non-zero ; :: thesis: contradiction
consider n1 being Element of NAT such that
A12: (seq " ) . n1 = 0c by A11, COMSEQ_1:4;
(seq . n1) " = (seq " ) . n1 by VALUED_1:10;
hence contradiction by A10, A12, XCMPLX_1:203, COMSEQ_1:4; :: thesis: verum

end;

then A13: h " is non-zero ;
A14: h (#) ((h " ) (#) (R1 /* h)) is convergent by A7, COMSEQ_2:29;
A15: lim (h (#) ((h " ) (#) (R1 /* h))) = 0 * 0 by A7, A9, COMSEQ_2:30
.= 0c ;
A16: (h " ) (#) ((R1 (#) R2) /* h) = ((R1 /* h) (#) (R2 /* h)) /" h by CFCONT_1:29
.= (((R1 /* h) (#) (R2 /* h)) (#) (h " )) /" (h (#) (h " )) by A13, COMSEQ_1:40
.= (((R1 /* h) (#) (R2 /* h)) (#) (h " )) (#) (((h " ) " ) (#) (h " )) by A13, COMSEQ_1:33
.= (h (#) (h " )) (#) ((R1 /* h) (#) ((h " ) (#) (R2 /* h))) by COMSEQ_1:11
.= ((h (#) (h " )) (#) (R1 /* h)) (#) ((h " ) (#) (R2 /* h)) by COMSEQ_1:11
.= (h (#) ((h " ) (#) (R1 /* h))) (#) ((h " ) (#) (R2 /* h)) by COMSEQ_1:11 ;
hence (h " ) (#) ((R1 (#) R2) /* h) is convergent by A8, A14, COMSEQ_2:29; :: thesis: lim ((h " ) (#) ((R1 (#) R2) /* h)) = 0c
thus lim ((h " ) (#) ((R1 (#) R2) /* h)) = 0c * 0c by A8, A14, A15, A16, COMSEQ_2:30
.= 0c ; :: thesis: verum

end;

hence for b₁ being PartFunc of COMPLEX ,COMPLEX st b₁ = R1 (#) R2 holds
( b₁ is total & b₁ is REST-like ) by Def3; :: thesis: verum