let R1, R2 be REST; :: thesis: ( R1 + R2 is REST & R1 - R2 is REST & R1 (#) R2 is REST )
A1: ( R1 is total & R2 is total ) by Def3;

now

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h " ) (#) ((R1 + R2) /* h) is convergent & lim ((h " ) (#) ((R1 + R2) /* h)) = 0 )
A3: ( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 ) by Def3;
A4: ( (h " ) (#) (R2 /* h) is convergent & lim ((h " ) (#) (R2 /* h)) = 0 ) by Def3;
A5: (h " ) (#) ((R1 + R2) /* h) = (h " ) (#) ((R1 /* h) + (R2 /* h)) by A1, RFUNCT_2:32
.= ((h " ) (#) (R1 /* h)) + ((h " ) (#) (R2 /* h)) by SEQ_1:24 ;
hence (h " ) (#) ((R1 + R2) /* h) is convergent by A3, A4, SEQ_2:19; :: thesis: lim ((h " ) (#) ((R1 + R2) /* h)) = 0
thus lim ((h " ) (#) ((R1 + R2) /* h)) = 0 + 0 by A3, A4, A5, SEQ_2:20
.= 0 ; :: thesis: verum

end;

hence R1 + R2 is REST by A1, Def3; :: thesis: ( R1 - R2 is REST & R1 (#) R2 is REST )

now

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h " ) (#) ((R1 - R2) /* h) is convergent & lim ((h " ) (#) ((R1 - R2) /* h)) = 0 )
A7: ( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 ) by Def3;
A8: ( (h " ) (#) (R2 /* h) is convergent & lim ((h " ) (#) (R2 /* h)) = 0 ) by Def3;
A9: (h " ) (#) ((R1 - R2) /* h) = (h " ) (#) ((R1 /* h) - (R2 /* h)) by A1, RFUNCT_2:32
.= ((h " ) (#) (R1 /* h)) - ((h " ) (#) (R2 /* h)) by SEQ_1:29 ;
hence (h " ) (#) ((R1 - R2) /* h) is convergent by A7, A8, SEQ_2:25; :: thesis: lim ((h " ) (#) ((R1 - R2) /* h)) = 0
thus lim ((h " ) (#) ((R1 - R2) /* h)) = 0 - 0 by A7, A8, A9, SEQ_2:26
.= 0 ; :: thesis: verum

end;

hence R1 - R2 is REST by A1, Def3; :: thesis: R1 (#) R2 is REST

now

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h " ) (#) ((R1 (#) R2) /* h) is convergent & lim ((h " ) (#) ((R1 (#) R2) /* h)) = 0 )
A11: ( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 ) by Def3;
A12: ( (h " ) (#) (R2 /* h) is convergent & lim ((h " ) (#) (R2 /* h)) = 0 ) by Def3;
A13: ( h is non-zero & h is convergent & lim h = 0 ) by Def1;
then A14: h " is non-zero by SEQ_1:41;
A15: h (#) ((h " ) (#) (R1 /* h)) is convergent by A11, A13, SEQ_2:28;
A16: lim (h (#) ((h " ) (#) (R1 /* h))) = 0 * 0 by A11, A13, SEQ_2:29
.= 0 ;
A17: (h " ) (#) ((R1 (#) R2) /* h) = ((R1 /* h) (#) (R2 /* h)) /" h by A1, RFUNCT_2:32
.= (((R1 /* h) (#) (R2 /* h)) (#) (h " )) /" (h (#) (h " )) by A14, SEQ_1:51
.= (((R1 /* h) (#) (R2 /* h)) (#) (h " )) (#) (((h " ) " ) (#) (h " )) by SEQ_1:44
.= (h (#) (h " )) (#) ((R1 /* h) (#) ((h " ) (#) (R2 /* h))) by SEQ_1:22
.= ((h (#) (h " )) (#) (R1 /* h)) (#) ((h " ) (#) (R2 /* h)) by SEQ_1:22
.= (h (#) ((h " ) (#) (R1 /* h))) (#) ((h " ) (#) (R2 /* h)) by SEQ_1:22 ;
hence (h " ) (#) ((R1 (#) R2) /* h) is convergent by A12, A15, SEQ_2:28; :: thesis: lim ((h " ) (#) ((R1 (#) R2) /* h)) = 0
thus lim ((h " ) (#) ((R1 (#) R2) /* h)) = 0 * 0 by A12, A15, A16, A17, SEQ_2:29
.= 0 ; :: thesis: verum

end;

hence R1 (#) R2 is REST by A1, Def3; :: thesis: verum