let L1 be LinearFunc; :: thesis: - L1 is LinearFunc
consider g1 being Real such that
A1: for p being Real holds L1 . p = g1 * p by FDIFF_1:def 3;
A2: L1 is total by FDIFF_1:def 3;

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

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

end;

hence - L1 is LinearFunc by A2, FDIFF_1:def 3; :: thesis: verum