now :: thesis: for h being non-zero 0 -convergent Complex_Sequence holds
( (h ") (#) ((R1 + R2) /* h) is convergent & lim ((h ") (#) ((R1 + R2) /* h)) = 0 )

let h be non-zero 0 -convergent 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:14
.= ((h ") (#) (R1 /* h)) + ((h ") (#) (R2 /* h)) by COMSEQ_1:10 ;
A2: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def3;
hence (h ") (#) ((R1 + R2) /* h) is convergent by A1; :: 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 RestFunc-like ) ; :: thesis: verum