let T, S be non trivial RealNormSpace; 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; ( R1 + R2 is REST of S,T & R1 - R2 is REST of S,T )
A1:
( R1 is total & R2 is total )
by Def5;
R1 + R2 is total
by A1, VFUNCT_1:32;
hence
R1 + R2 is REST of S,T
by A2, Def5; R1 - R2 is REST of S,T
R1 - R2 is total
by A1, VFUNCT_1:32;
hence
R1 - R2 is REST of S,T
by A5, Def5; verum