now

let h be convergent_to_0 Complex_Sequence; :: thesis: ( (h " ) (#) ((R1 - R2) /* h) is convergent & lim ((h " ) (#) ((R1 - R2) /* h)) = 0c )
A4: ( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0c ) by Def3;
A5: ( (h " ) (#) (R2 /* h) is convergent & lim ((h " ) (#) (R2 /* h)) = 0c ) by Def3;
A6: (h " ) (#) ((R1 - R2) /* h) = (h " ) (#) ((R1 /* h) - (R2 /* h)) by CFCONT_1:29
.= ((h " ) (#) (R1 /* h)) - ((h " ) (#) (R2 /* h)) by COMSEQ_1:18 ;
hence (h " ) (#) ((R1 - R2) /* h) is convergent by A4, A5, COMSEQ_2:25; :: thesis: lim ((h " ) (#) ((R1 - R2) /* h)) = 0c
thus lim ((h " ) (#) ((R1 - R2) /* h)) = 0c - 0c by A4, A5, A6, COMSEQ_2:26
.= 0c ; :: thesis: verum

end;

hence R1 - R2 is C_REST by Def3; :: thesis: verum