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
( (||.h.|| ") (#) ((R1 + R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = 0. T )
let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( (||.h.|| ") (#) ((R1 + R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = 0. T ) )
assume A3: h is non-zero ; :: thesis: ( (||.h.|| ") (#) ((R1 + R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = 0. T )
A4: ( (||.h.|| ") (#) (R1 /* h) is convergent & (||.h.|| ") (#) (R2 /* h) is convergent ) by Def5, A3;
A5: (||.h.|| ") (#) ((R1 + R2) /* h) = (||.h.|| ") (#) ((R1 /* h) + (R2 /* h)) by A1, Th25
.= ((||.h.|| ") (#) (R1 /* h)) + ((||.h.|| ") (#) (R2 /* h)) by Th9 ;
hence (||.h.|| ") (#) ((R1 + R2) /* h) is convergent by A4, NORMSP_1:19; :: thesis: lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = 0. T
( lim ((||.h.|| ") (#) (R1 /* h)) = 0. T & lim ((||.h.|| ") (#) (R2 /* h)) = 0. T ) by A3, Def5;
hence lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = (0. T) + (0. T) by A4, A5, NORMSP_1:25
.= 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
( (||.h.|| ") (#) ((R1 - R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = 0. T )
let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( (||.h.|| ") (#) ((R1 - R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = 0. T ) )
assume A7: h is non-zero ; :: thesis: ( (||.h.|| ") (#) ((R1 - R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = 0. T )
A8: ( (||.h.|| ") (#) (R1 /* h) is convergent & (||.h.|| ") (#) (R2 /* h) is convergent ) by Def5, A7;
A9: (||.h.|| ") (#) ((R1 - R2) /* h) = (||.h.|| ") (#) ((R1 /* h) - (R2 /* h)) by A1, Th25
.= ((||.h.|| ") (#) (R1 /* h)) - ((||.h.|| ") (#) (R2 /* h)) by Th12 ;
hence (||.h.|| ") (#) ((R1 - R2) /* h) is convergent by A8, NORMSP_1:20; :: thesis: lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = 0. T
( lim ((||.h.|| ") (#) (R1 /* h)) = 0. T & lim ((||.h.|| ") (#) (R2 /* h)) = 0. T ) by Def5, A7;
hence lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = (0. T) - (0. T) by A8, A9, NORMSP_1:26
.= 0. T by RLVECT_1:13 ;
:: thesis: verum
end;
R1 + R2 is total by A1, VFUNCT_1:32;
hence R1 + R2 is RestFunc of S,T by A2, Def5; :: thesis: R1 - R2 is RestFunc of S,T
R1 - R2 is total by A1, VFUNCT_1:32;
hence R1 - R2 is RestFunc of S,T by A6, Def5; :: thesis: verum