let F be RealNormSpace; :: thesis: for L1, L2 being LinearFunc of F holds
( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc of F )
let L1, L2 be LinearFunc of F; :: thesis: ( L1 + L2 is LinearFunc of F & L1 - L2 is LinearFunc 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;

now :: thesis: for p being Real holds (L1 + L2) /. p = p * (g1 + g2)

let p be Real; :: thesis: (L1 + L2) /. p = p * (g1 + g2)
reconsider pp = p as Element of REAL by XREAL_0:def 1;
thus (L1 + L2) /. p = (L1 /. pp) + (L2 /. pp) by VFUNCT_1:37
.= (p * g1) + (L2 /. pp) by A1
.= (p * g1) + (p * g2) by A2
.= p * (g1 + g2) by RLVECT_1:def 5 ; :: thesis: verum

end;

hence L1 + L2 is LinearFunc of F by A3, Def2; :: thesis: L1 - L2 is LinearFunc of F
A4: L1 - L2 is total by VFUNCT_1:32;

now :: thesis: for p being Real holds (L1 - L2) /. p = p * (g1 - g2)

let p be Real; :: thesis: (L1 - L2) /. p = p * (g1 - g2)
reconsider pp = p as Element of REAL by XREAL_0:def 1;
thus (L1 - L2) /. p = (L1 /. pp) - (L2 /. pp) by VFUNCT_1:37
.= (p * g1) - (L2 /. pp) by A1
.= (p * g1) - (p * g2) by A2
.= p * (g1 - g2) by RLVECT_1:34 ; :: thesis: verum

end;

hence L1 - L2 is LinearFunc of F by A4, Def2; :: thesis: verum