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;

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

hence
L1 + L2 is LinearFunc
by A3, Def3; :: thesis: L1 - L2 is LinearFunclet 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;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

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

hence
L1 - L2 is LinearFunc
by A3, Def3; :: thesis: verumlet 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;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