let T, S be non trivial RealNormSpace; :: thesis: for R1, R2 being REST of S,T holds
( R1 + R2 is REST of S,T & R1 - R2 is REST of S,T )
let R1, R2 be REST of S,T; :: thesis: ( R1 + R2 is REST of S,T & R1 - R2 is REST of S,T )
A1:
( R1 is total & R2 is total )
by Def5;
then A2:
R1 + R2 is total
by VFUNCT_1:38;
hence
R1 + R2 is REST of S,T
by A2, Def5; :: thesis: R1 - R2 is REST of S,T
A6:
R1 - R2 is total
by A1, VFUNCT_1:38;
hence
R1 - R2 is REST of S,T
by A6, Def5; :: thesis: verum