let S, T be RealNormSpace; :: thesis: for R1, R2 being RestFunc of S,T holds
( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T )

let R1, R2 be RestFunc of S,T; :: thesis: ( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T )
A1: ( R1 is total & R2 is total ) by Def5;
A2: now :: thesis: for h being 0. S -convergent sequence of S st h is non-zero holds
( () (#) ((R1 + R2) /* h) is convergent & lim (() (#) ((R1 + R2) /* h)) = 0. T )
let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( () (#) ((R1 + R2) /* h) is convergent & lim (() (#) ((R1 + R2) /* h)) = 0. T ) )
assume A3: h is non-zero ; :: thesis: ( () (#) ((R1 + R2) /* h) is convergent & lim (() (#) ((R1 + R2) /* h)) = 0. T )
A4: ( (||.h.|| ") (#) (R1 /* h) is convergent & () (#) (R2 /* h) is convergent ) by ;
A5: () (#) ((R1 + R2) /* h) = () (#) ((R1 /* h) + (R2 /* h)) by
.= (() (#) (R1 /* h)) + (() (#) (R2 /* h)) by Th9 ;
hence (||.h.|| ") (#) ((R1 + R2) /* h) is convergent by ; :: thesis: lim (() (#) ((R1 + R2) /* h)) = 0. T
( lim (() (#) (R1 /* h)) = 0. T & lim (() (#) (R2 /* h)) = 0. T ) by ;
hence lim (() (#) ((R1 + R2) /* h)) = (0. T) + (0. T) by
.= 0. T by RLVECT_1:4 ;
:: thesis: verum
end;
A6: now :: thesis: for h being 0. S -convergent sequence of S st h is non-zero holds
( () (#) ((R1 - R2) /* h) is convergent & lim (() (#) ((R1 - R2) /* h)) = 0. T )
let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( () (#) ((R1 - R2) /* h) is convergent & lim (() (#) ((R1 - R2) /* h)) = 0. T ) )
assume A7: h is non-zero ; :: thesis: ( () (#) ((R1 - R2) /* h) is convergent & lim (() (#) ((R1 - R2) /* h)) = 0. T )
A8: ( (||.h.|| ") (#) (R1 /* h) is convergent & () (#) (R2 /* h) is convergent ) by ;
A9: () (#) ((R1 - R2) /* h) = () (#) ((R1 /* h) - (R2 /* h)) by
.= (() (#) (R1 /* h)) - (() (#) (R2 /* h)) by Th12 ;
hence (||.h.|| ") (#) ((R1 - R2) /* h) is convergent by ; :: thesis: lim (() (#) ((R1 - R2) /* h)) = 0. T
( lim (() (#) (R1 /* h)) = 0. T & lim (() (#) (R2 /* h)) = 0. T ) by ;
hence lim (() (#) ((R1 - R2) /* h)) = (0. T) - (0. T) by
.= 0. T by RLVECT_1:13 ;
:: thesis: verum
end;
R1 + R2 is total by ;
hence R1 + R2 is RestFunc of S,T by ; :: thesis: R1 - R2 is RestFunc of S,T
R1 - R2 is total by ;
hence R1 - R2 is RestFunc of S,T by ; :: thesis: verum