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

now

let p be Real; :: thesis: (L1 + L2) . p = (g1 + g2) * p
thus (L1 + L2) . p = (L1 . p) + (L2 . p) by A3, RFUNCT_1:72
.= (g1 * p) + (L2 . p) by A1
.= (g1 * p) + (g2 * p) by A2
.= (g1 + g2) * p ; :: thesis: verum

end;

hence L1 + L2 is LINEAR by A3, Def4; :: thesis: L1 - L2 is LINEAR

now

let p be Real; :: thesis: (L1 - L2) . p = (g1 - g2) * p
thus (L1 - L2) . p = (L1 . p) - (L2 . p) by A3, RFUNCT_1:72
.= (g1 * p) - (L2 . p) by A1
.= (g1 * p) - (g2 * p) by A2
.= (g1 - g2) * p ; :: thesis: verum

end;

hence L1 - L2 is LINEAR by A3, Def4; :: thesis: verum