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:13
.= ((h ") (#) (R1 /* h)) + ((h ") (#) (R2 /* h)) by SEQ_1:16 ;
A3: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def3;
hence (h ") (#) ((R1 + R2) /* h) is convergent by A2, SEQ_2:5; :: 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:6
.= 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:13
.= ((h ") (#) (R1 /* h)) - ((h ") (#) (R2 /* h)) by SEQ_1:21 ;
A5: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def3;
hence (h ") (#) ((R1 - R2) /* h) is convergent by A4, SEQ_2:11; :: 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:12
.= 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:33;
A8: ( (h ") (#) (R1 /* h) is convergent & h is convergent ) by Def1, Def3;
then A9: h (#) ((h ") (#) (R1 /* h)) is convergent by SEQ_2:14;
( lim ((h ") (#) (R1 /* h)) = 0 & lim h = 0 ) by Def1, Def3;
then A10: lim (h (#) ((h ") (#) (R1 /* h))) = 0 * 0 by A8, SEQ_2:15
.= 0 ;
A11: (h ") (#) ((R1 (#) R2) /* h) = ((R1 /* h) (#) (R2 /* h)) /" h by A1, RFUNCT_2:13
.= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) /" (h (#) (h ")) by A7, SEQ_1:43
.= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) (#) (((h ") ") (#) (h ")) by SEQ_1:36
.= (h (#) (h ")) (#) ((R1 /* h) (#) ((h ") (#) (R2 /* h))) by SEQ_1:14
.= ((h (#) (h ")) (#) (R1 /* h)) (#) ((h ") (#) (R2 /* h)) by SEQ_1:14
.= (h (#) ((h ") (#) (R1 /* h))) (#) ((h ") (#) (R2 /* h)) by SEQ_1:14 ;
hence (h ") (#) ((R1 (#) R2) /* h) is convergent by A6, A9, SEQ_2:14; :: 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:15
.= 0 ;
:: thesis: verum

end;

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