let L1, L2 be LinearFunc; :: thesis: ( L1 + L2 is LinearFunc & L1 - L2 is LinearFunc )
consider g1 being Real such that
A1: for p being Real holds L1 . p = g1 * p by Def3;
consider g2 being Real such that
A2: for p being Real holds L2 . p = g2 * p by Def3;
A3: ( L1 is total & L2 is total ) by Def3;

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

let p be Real; :: thesis: (L1 + L2) . p = (g1 + g2) * p
reconsider pp = p as Element of REAL by XREAL_0:def 1;
thus (L1 + L2) . p = (L1 . pp) + (L2 . pp) by A3, RFUNCT_1:56
.= (g1 * p) + (L2 . p) by A1
.= (g1 * p) + (g2 * p) by A2
.= (g1 + g2) * p ; :: thesis: verum

end;

hence L1 + L2 is LinearFunc by A3, Def3; :: thesis: L1 - L2 is LinearFunc

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

let p be Real; :: thesis: (L1 - L2) . p = (g1 - g2) * p
reconsider pp = p as Element of REAL by XREAL_0:def 1;
thus (L1 - L2) . p = (L1 . pp) - (L2 . pp) by A3, RFUNCT_1:56
.= (g1 * p) - (L2 . p) by A1
.= (g1 * p) - (g2 * p) by A2
.= (g1 - g2) * p ; :: thesis: verum

end;

hence L1 - L2 is LinearFunc by A3, Def3; :: thesis: verum