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
.= ((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
.= 0 ;
:: thesis: verum
end;
hence R1 + R2 is RestFunc by ; :: 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
.= ((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
.= 0 ;
:: thesis: verum
end;
hence R1 - R2 is RestFunc by ; :: 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
.= 0 ;
A11: (h ") (#) ((R1 (#) R2) /* h) = ((R1 /* h) (#) (R2 /* h)) /" h by
.= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) /" (h (#) (h ")) by
.= (((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
.= 0 ;
:: thesis: verum
end;
hence R1 (#) R2 is RestFunc by ; :: thesis: verum