let F be non trivial RealNormSpace; :: thesis: for L1, L2 being LINEAR of F holds
( L1 + L2 is LINEAR of F & L1 - L2 is LINEAR of F )
let L1, L2 be LINEAR of F; :: thesis: ( L1 + L2 is LINEAR of F & L1 - L2 is LINEAR of F )
consider g1 being Point of F such that
A1: for p being Real holds L1 . p = p * g1 by Def2;
consider g2 being Point of F such that
A2: for p being Real holds L2 . p = p * g2 by Def2;
A3: L1 + L2 is total by VFUNCT_1:32;
then A4: dom (L1 + L2) = REAL by FUNCT_2:def 1;

now

let p be Real; :: thesis: (L1 + L2) . p = p * (g1 + g2)
thus (L1 + L2) . p = (L1 + L2) /. p by A4, PARTFUN1:def 6
.= (L1 /. p) + (L2 /. p) by VFUNCT_1:37
.= (p * g1) + (L2 . p) by A1
.= (p * g1) + (p * g2) by A2
.= p * (g1 + g2) by RLVECT_1:def 5 ; :: thesis: verum

end;

hence L1 + L2 is LINEAR of F by A3, Def2; :: thesis: L1 - L2 is LINEAR of F
A5: L1 - L2 is total by VFUNCT_1:32;
then A6: dom (L1 - L2) = REAL by FUNCT_2:def 1;

now

let p be Real; :: thesis: (L1 - L2) . p = p * (g1 - g2)
thus (L1 - L2) . p = (L1 - L2) /. p by A6, PARTFUN1:def 6
.= (L1 /. p) - (L2 /. p) by VFUNCT_1:37
.= (p * g1) - (L2 . p) by A1
.= (p * g1) - (p * g2) by A2
.= p * (g1 - g2) by RLVECT_1:34 ; :: thesis: verum

end;

hence L1 - L2 is LINEAR of F by A5, Def2; :: thesis: verum