now

let h be convergent_to_0 Complex_Sequence; :: thesis: ( (h " ) (#) ((R1 + R2) /* h) is convergent & lim ((h " ) (#) ((R1 + R2) /* h)) = 0 )
A1: (h " ) (#) ((R1 + R2) /* h) = (h " ) (#) ((R1 /* h) + (R2 /* h)) by CFCONT_1:29
.= ((h " ) (#) (R1 /* h)) + ((h " ) (#) (R2 /* h)) by COMSEQ_1:13 ;
A2: ( (h " ) (#) (R1 /* h) is convergent & (h " ) (#) (R2 /* h) is convergent ) by Def3;
hence (h " ) (#) ((R1 + R2) /* h) is convergent by A1, COMSEQ_2:13; :: thesis: lim ((h " ) (#) ((R1 + R2) /* h)) = 0
A3: lim ((h " ) (#) (R1 /* h)) = 0 by Def3;
thus lim ((h " ) (#) ((R1 + R2) /* h)) = (lim ((h " ) (#) (R1 /* h))) + (lim ((h " ) (#) (R2 /* h))) by A2, A1, COMSEQ_2:14
.= 0 by A3, Def3 ; :: 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