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 )
A2: (h " ) (#) ((R1 + R2) /* h) = (h " ) (#) ((R1 /* h) + (R2 /* h)) by A1, RFUNCT_2:32
.= ((h " ) (#) (R1 /* h)) + ((h " ) (#) (R2 /* h)) by SEQ_1:24 ;
A3: ( (h " ) (#) (R1 /* h) is convergent & (h " ) (#) (R2 /* h) is convergent ) by Def3;
hence (h " ) (#) ((R1 + R2) /* h) is convergent by A2, SEQ_2:19; :: thesis: lim ((h " ) (#) ((R1 + R2) /* h)) = 0
( lim ((h " ) (#) (R1 /* h)) = 0 & lim ((h " ) (#) (R2 /* h)) = 0 ) by Def3;
hence lim ((h " ) (#) ((R1 + R2) /* h)) = 0 + 0 by A3, A2, 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 )
A4: (h " ) (#) ((R1 - R2) /* h) = (h " ) (#) ((R1 /* h) - (R2 /* h)) by A1, RFUNCT_2:32
.= ((h " ) (#) (R1 /* h)) - ((h " ) (#) (R2 /* h)) by SEQ_1:29 ;
A5: ( (h " ) (#) (R1 /* h) is convergent & (h " ) (#) (R2 /* h) is convergent ) by Def3;
hence (h " ) (#) ((R1 - R2) /* h) is convergent by A4, SEQ_2:25; :: thesis: lim ((h " ) (#) ((R1 - R2) /* h)) = 0
( lim ((h " ) (#) (R1 /* h)) = 0 & lim ((h " ) (#) (R2 /* h)) = 0 ) by Def3;
hence lim ((h " ) (#) ((R1 - R2) /* h)) = 0 - 0 by A5, A4, 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 )
A6: (h " ) (#) (R2 /* h) is convergent by Def3;
h is non-zero by Def1;
then A7: h " is non-zero by SEQ_1:41;
A8: ( (h " ) (#) (R1 /* h) is convergent & h is convergent ) by Def1, Def3;
then A9: h (#) ((h " ) (#) (R1 /* h)) is convergent by SEQ_2:28;
( lim ((h " ) (#) (R1 /* h)) = 0 & lim h = 0 ) by Def1, Def3;
then A10: lim (h (#) ((h " ) (#) (R1 /* h))) = 0 * 0 by A8, SEQ_2:29
.= 0 ;
A11: (h " ) (#) ((R1 (#) R2) /* h) = ((R1 /* h) (#) (R2 /* h)) /" h by A1, RFUNCT_2:32
.= (((R1 /* h) (#) (R2 /* h)) (#) (h " )) /" (h (#) (h " )) by A7, 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 A6, A9, SEQ_2:28; :: thesis: lim ((h " ) (#) ((R1 (#) R2) /* h)) = 0
lim ((h " ) (#) (R2 /* h)) = 0 by Def3;
hence lim ((h " ) (#) ((R1 (#) R2) /* h)) = 0 * 0 by A6, A9, A10, A11, SEQ_2:29
.= 0 ;
:: thesis: verum

end;

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