let F be RealNormSpace; :: thesis: for R1, R2 being RestFunc of F holds
( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F )
let R1, R2 be RestFunc of F; :: thesis: ( R1 + R2 is RestFunc of F & R1 - R2 is RestFunc of F )
A1: ( R1 is total & R2 is total ) by Def1;

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

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((R1 + R2) /* h) is convergent & lim ((h ") (#) ((R1 + R2) /* h)) = 0. F )
A3: (h ") (#) ((R1 + R2) /* h) = (h ") (#) ((R1 /* h) + (R2 /* h)) by A1, Th6
.= ((h ") (#) (R1 /* h)) + ((h ") (#) (R2 /* h)) by NDIFF_1:9 ;
A4: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def1;
hence (h ") (#) ((R1 + R2) /* h) is convergent by A3, NORMSP_1:19; :: thesis: lim ((h ") (#) ((R1 + R2) /* h)) = 0. F
( lim ((h ") (#) (R1 /* h)) = 0. F & lim ((h ") (#) (R2 /* h)) = 0. F ) by Def1;
hence lim ((h ") (#) ((R1 + R2) /* h)) = (0. F) + (0. F) by A4, A3, NORMSP_1:25
.= 0. F by RLVECT_1:def 4 ;
:: thesis: verum

end;

R1 + R2 is total by A1, VFUNCT_1:32;
hence R1 + R2 is RestFunc of F by A2, Def1; :: thesis: R1 - R2 is RestFunc of F

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

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((R1 - R2) /* h) is convergent & lim ((h ") (#) ((R1 - R2) /* h)) = 0. F )
A6: (h ") (#) ((R1 - R2) /* h) = (h ") (#) ((R1 /* h) - (R2 /* h)) by A1, Th6
.= ((h ") (#) (R1 /* h)) - ((h ") (#) (R2 /* h)) by NDIFF_1:12 ;
A7: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def1;
hence (h ") (#) ((R1 - R2) /* h) is convergent by A6, NORMSP_1:20; :: thesis: lim ((h ") (#) ((R1 - R2) /* h)) = 0. F
( lim ((h ") (#) (R1 /* h)) = 0. F & lim ((h ") (#) (R2 /* h)) = 0. F ) by Def1;
hence lim ((h ") (#) ((R1 - R2) /* h)) = (0. F) - (0. F) by A7, A6, NORMSP_1:26
.= 0. F by RLVECT_1:13 ;
:: thesis: verum

end;

R1 - R2 is total by A1, VFUNCT_1:32;
hence R1 - R2 is RestFunc of F by A5, Def1; :: thesis: verum