let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL holds
( - (f + g) = (- f) + (- g) & - (f - g) = (- f) + g & - (f - g) = g - f & - ((- f) + g) = f - g & - ((- f) + g) = f + (- g) )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( - (f + g) = (- f) + (- g) & - (f - g) = (- f) + g & - (f - g) = g - f & - ((- f) + g) = f - g & - ((- f) + g) = f + (- g) )
A1: ( f " {-infty} = (- f) " {+infty} & f " {+infty} = (- f) " {-infty} & g " {-infty} = (- g) " {+infty} & g " {+infty} = (- g) " {-infty} ) by LEM10;
A2: ( dom f = dom (- f) & dom g = dom (- g) ) by MESFUNC1:def 7;
A3: ( dom (- (f + g)) = dom (f + g) & dom (- f) = dom f & dom (- g) = dom g & dom (- (f - g)) = dom (f - g) ) by MESFUNC1:def 7;
then A4: dom (- (f + g)) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;
then A5: dom (- (f + g)) = dom ((- f) + (- g)) by A1, A2, MESFUNC1:def 3;
A6: dom (- (f - g)) = ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty}))) by A3, MESFUNC1:def 4;
then A7: dom (- (f - g)) = dom ((- f) + g) by A1, A2, MESFUNC1:def 3;
then C1: dom (- ((- f) + g)) = dom (- (f - g)) by MESFUNC1:def 7;
then A10: dom (- ((- f) + g)) = dom (f - g) by MESFUNC1:def 7;
then dom (- ((- f) + g)) = ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty}))) by MESFUNC1:def 4;
then A12: dom (- ((- f) + g)) = dom (f + (- g)) by A1, A2, MESFUNC1:def 3;
A8: dom (- (f - g)) = dom (g - f) by A6, MESFUNC1:def 4;
A9: dom (- ((- f) + g)) = dom ((- f) + g) by MESFUNC1:def 7;
B3: ( dom (- (f + g)) c= dom f & dom (- (f + g)) c= dom g ) by A4, XBOOLE_1:18, XBOOLE_1:36;
B4: ( dom (- (f - g)) c= dom f & dom (- (f - g)) c= dom g ) by A6, XBOOLE_1:18, XBOOLE_1:36;
B5: ( dom (- ((- f) + g)) c= dom (- f) & dom (- ((- f) + g)) c= dom g ) by C1, A3, A6, XBOOLE_1:18, XBOOLE_1:36;

now :: thesis: for x being Element of X st x in dom (- (f + g)) holds
(- (f + g)) . x = ((- f) + (- g)) . x

let x be Element of X; :: thesis: ( x in dom (- (f + g)) implies (- (f + g)) . x = ((- f) + (- g)) . x )
assume B2: x in dom (- (f + g)) ; :: thesis: (- (f + g)) . x = ((- f) + (- g)) . x
then (- (f + g)) . x = - ((f + g) . x) by MESFUNC1:def 7
.= - ((f . x) + (g . x)) by A3, B2, MESFUNC1:def 3
.= (- (f . x)) + (- (g . x)) by XXREAL_3:9
.= ((- f) . x) + (- (g . x)) by A2, B2, B3, MESFUNC1:def 7
.= ((- f) . x) + ((- g) . x) by A2, B2, B3, MESFUNC1:def 7 ;
hence (- (f + g)) . x = ((- f) + (- g)) . x by B2, A5, MESFUNC1:def 3; :: thesis: verum

end;

hence - (f + g) = (- f) + (- g) by A5, PARTFUN1:5; :: thesis: ( - (f - g) = (- f) + g & - (f - g) = g - f & - ((- f) + g) = f - g & - ((- f) + g) = f + (- g) )

now :: thesis: for x being Element of X st x in dom (- (f - g)) holds
(- (f - g)) . x = ((- f) + g) . x

let x be Element of X; :: thesis: ( x in dom (- (f - g)) implies (- (f - g)) . x = ((- f) + g) . x )
assume B2: x in dom (- (f - g)) ; :: thesis: (- (f - g)) . x = ((- f) + g) . x
then (- (f - g)) . x = - ((f - g) . x) by MESFUNC1:def 7
.= - ((f . x) - (g . x)) by A3, B2, MESFUNC1:def 4
.= (- (f . x)) + (g . x) by XXREAL_3:26
.= ((- f) . x) + (g . x) by A2, B4, B2, MESFUNC1:def 7 ;
hence (- (f - g)) . x = ((- f) + g) . x by B2, A7, MESFUNC1:def 3; :: thesis: verum

end;

hence - (f - g) = (- f) + g by A7, PARTFUN1:5; :: thesis: ( - (f - g) = g - f & - ((- f) + g) = f - g & - ((- f) + g) = f + (- g) )

now :: thesis: for x being Element of X st x in dom (- (f - g)) holds
(- (f - g)) . x = (g - f) . x

let x be Element of X; :: thesis: ( x in dom (- (f - g)) implies (- (f - g)) . x = (g - f) . x )
assume B2: x in dom (- (f - g)) ; :: thesis: (- (f - g)) . x = (g - f) . x
then (- (f - g)) . x = - ((f - g) . x) by MESFUNC1:def 7
.= - ((f . x) - (g . x)) by A3, B2, MESFUNC1:def 4
.= (g . x) - (f . x) by XXREAL_3:26 ;
hence (- (f - g)) . x = (g - f) . x by B2, A8, MESFUNC1:def 4; :: thesis: verum

end;

hence - (f - g) = g - f by A8, PARTFUN1:5; :: thesis: ( - ((- f) + g) = f - g & - ((- f) + g) = f + (- g) )

now :: thesis: for x being Element of X st x in dom (- ((- f) + g)) holds
(- ((- f) + g)) . x = (f - g) . x

let x be Element of X; :: thesis: ( x in dom (- ((- f) + g)) implies (- ((- f) + g)) . x = (f - g) . x )
assume B2: x in dom (- ((- f) + g)) ; :: thesis: (- ((- f) + g)) . x = (f - g) . x
then (- ((- f) + g)) . x = - (((- f) + g) . x) by MESFUNC1:def 7
.= - (((- f) . x) + (g . x)) by A9, B2, MESFUNC1:def 3
.= - ((- (f . x)) + (g . x)) by B5, B2, MESFUNC1:def 7
.= (f . x) - (g . x) by XXREAL_3:27 ;
hence (- ((- f) + g)) . x = (f - g) . x by B2, A10, MESFUNC1:def 4; :: thesis: verum

end;

hence - ((- f) + g) = f - g by A10, PARTFUN1:5; :: thesis: - ((- f) + g) = f + (- g)

now :: thesis: for x being Element of X st x in dom (- ((- f) + g)) holds
(- ((- f) + g)) . x = (f + (- g)) . x

let x be Element of X; :: thesis: ( x in dom (- ((- f) + g)) implies (- ((- f) + g)) . x = (f + (- g)) . x )
assume B2: x in dom (- ((- f) + g)) ; :: thesis: (- ((- f) + g)) . x = (f + (- g)) . x
then (- ((- f) + g)) . x = - (((- f) + g) . x) by MESFUNC1:def 7
.= - (((- f) . x) + (g . x)) by A9, B2, MESFUNC1:def 3
.= - ((- (f . x)) + (g . x)) by B5, B2, MESFUNC1:def 7
.= (f . x) + (- (g . x)) by XXREAL_3:27
.= (f . x) + ((- g) . x) by B2, B5, A3, MESFUNC1:def 7 ;
hence (- ((- f) + g)) . x = (f + (- g)) . x by B2, A12, MESFUNC1:def 3; :: thesis: verum

end;

hence - ((- f) + g) = f + (- g) by A12, PARTFUN1:5; :: thesis: verum