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

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

let h be non-zero 0 -convergent 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 Def2;
hence (h ") (#) ((R1 + R2) /* h) is convergent by A2; :: thesis: lim ((h ") (#) ((R1 + R2) /* h)) = 0
( lim ((h ") (#) (R1 /* h)) = 0 & lim ((h ") (#) (R2 /* h)) = 0 ) by Def2;
hence lim ((h ") (#) ((R1 + R2) /* h)) = 0 + 0 by A3, A2, SEQ_2:6
.= 0 ;
:: thesis: verum

end;

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

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

let h be non-zero 0 -convergent 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 Def2;
hence (h ") (#) ((R1 - R2) /* h) is convergent by A4; :: thesis: lim ((h ") (#) ((R1 - R2) /* h)) = 0
( lim ((h ") (#) (R1 /* h)) = 0 & lim ((h ") (#) (R2 /* h)) = 0 ) by Def2;
hence lim ((h ") (#) ((R1 - R2) /* h)) = 0 - 0 by A5, A4, SEQ_2:12
.= 0 ;
:: thesis: verum

end;

hence R1 - R2 is RestFunc by A1, Def2; :: thesis: R1 (#) R2 is RestFunc

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

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((R1 (#) R2) /* h) is convergent & lim ((h ") (#) ((R1 (#) R2) /* h)) = 0 )
A6: (h ") (#) (R2 /* h) is convergent by Def2;
A7: h " is non-zero by SEQ_1:33;
A8: ( (h ") (#) (R1 /* h) is convergent & h is convergent ) by Def2;
then A9: h (#) ((h ") (#) (R1 /* h)) is convergent ;
( lim ((h ") (#) (R1 /* h)) = 0 & lim h = 0 ) by Def2;
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; :: thesis: lim ((h ") (#) ((R1 (#) R2) /* h)) = 0
lim ((h ") (#) (R2 /* h)) = 0 by Def2;
hence lim ((h ") (#) ((R1 (#) R2) /* h)) = 0 * 0 by A6, A9, A10, A11, SEQ_2:15
.= 0 ;
:: thesis: verum

end;

hence R1 (#) R2 is RestFunc by A1, Def2; :: thesis: verum