let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,ExtREAL holds f1 - f2 = f1 + (- f2)
let f1, f2 be PartFunc of C,ExtREAL; :: thesis: f1 - f2 = f1 + (- f2)
A1: dom (f1 - f2) = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by MESFUNC1:def 4;
for x being Element of C st x in f2 " {+infty} holds
x in (- f2) " {-infty}

proof

let x be Element of C; :: thesis: ( x in f2 " {+infty} implies x in (- f2) " {-infty} )
assume A3: x in f2 " {+infty} ; :: thesis: x in (- f2) " {-infty}
then A4: x in dom f2 by FUNCT_1:def 13;
A5: f2 . x in {+infty} by A3, FUNCT_1:def 13;
A6: x in dom (- f2) by A4, MESFUNC1:def 7;
f2 . x = +infty by A5, TARSKI:def 1;
then (- f2) . x = - +infty by A6, MESFUNC1:def 7
.= -infty by XXREAL_3:def 3 ;
then (- f2) . x in {-infty} by TARSKI:def 1;
hence x in (- f2) " {-infty} by A6, FUNCT_1:def 13; :: thesis: verum

end;

then A10: f2 " {+infty} c= (- f2) " {-infty} by SUBSET_1:7;
for x being Element of C st x in (- f2) " {-infty} holds
x in f2 " {+infty}

proof

let x be Element of C; :: thesis: ( x in (- f2) " {-infty} implies x in f2 " {+infty} )
assume A12: x in (- f2) " {-infty} ; :: thesis: x in f2 " {+infty}
then A13: x in dom (- f2) by FUNCT_1:def 13;
A14: (- f2) . x in {-infty} by A12, FUNCT_1:def 13;
A15: x in dom f2 by A13, MESFUNC1:def 7;
(- f2) . x = -infty by A14, TARSKI:def 1;
then -infty = - (f2 . x) by A13, MESFUNC1:def 7;
then f2 . x in {+infty} by TARSKI:def 1, XXREAL_3:5;
hence x in f2 " {+infty} by A15, FUNCT_1:def 13; :: thesis: verum

end;

then (- f2) " {-infty} c= f2 " {+infty} by SUBSET_1:7;
then A20: f2 " {+infty} = (- f2) " {-infty} by A10, XBOOLE_0:def 10;
for x being Element of C st x in f2 " {-infty} holds
x in (- f2) " {+infty}

proof

let x be Element of C; :: thesis: ( x in f2 " {-infty} implies x in (- f2) " {+infty} )
assume A22: x in f2 " {-infty} ; :: thesis: x in (- f2) " {+infty}
then A23: x in dom f2 by FUNCT_1:def 13;
A24: f2 . x in {-infty} by A22, FUNCT_1:def 13;
A25: x in dom (- f2) by A23, MESFUNC1:def 7;
f2 . x = -infty by A24, TARSKI:def 1;
then (- f2) . x = +infty by A25, MESFUNC1:def 7, XXREAL_3:5;
then (- f2) . x in {+infty} by TARSKI:def 1;
hence x in (- f2) " {+infty} by A25, FUNCT_1:def 13; :: thesis: verum

end;

then A29: f2 " {-infty} c= (- f2) " {+infty} by SUBSET_1:7;
for x being Element of C st x in (- f2) " {+infty} holds
x in f2 " {-infty}

proof

let x be Element of C; :: thesis: ( x in (- f2) " {+infty} implies x in f2 " {-infty} )
assume A31: x in (- f2) " {+infty} ; :: thesis: x in f2 " {-infty}
then A32: x in dom (- f2) by FUNCT_1:def 13;
A33: (- f2) . x in {+infty} by A31, FUNCT_1:def 13;
A34: x in dom f2 by A32, MESFUNC1:def 7;
(- f2) . x = +infty by A33, TARSKI:def 1;
then +infty = - (f2 . x) by A32, MESFUNC1:def 7;
then f2 . x = - +infty
.= -infty by XXREAL_3:def 3 ;
then f2 . x in {-infty} by TARSKI:def 1;
hence x in f2 " {-infty} by A34, FUNCT_1:def 13; :: thesis: verum

end;

then (- f2) " {+infty} c= f2 " {-infty} by SUBSET_1:7;
then A40: f2 " {-infty} = (- f2) " {+infty} by A29, XBOOLE_0:def 10;
dom (f1 + (- f2)) = ((dom f1) /\ (dom (- f2))) \ (((f1 " {-infty}) /\ ((- f2) " {+infty})) \/ ((f1 " {+infty}) /\ ((- f2) " {-infty}))) by MESFUNC1:def 3
.= ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {-infty})) \/ ((f1 " {+infty}) /\ (f2 " {+infty}))) by A20, A40, MESFUNC1:def 7 ;
then A42: dom (f1 - f2) = dom (f1 + (- f2)) by MESFUNC1:def 4;
for x being Element of C st x in dom (f1 - f2) holds
(f1 - f2) . x = (f1 + (- f2)) . x

proof

let x be Element of C; :: thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (f1 + (- f2)) . x )
assume A44: x in dom (f1 - f2) ; :: thesis: (f1 - f2) . x = (f1 + (- f2)) . x
dom (f1 - f2) c= (dom f1) /\ (dom f2) by A1, XBOOLE_1:36;
then x in dom f2 by A44, XBOOLE_0:def 4;
then A47: x in dom (- f2) by MESFUNC1:def 7;
( (f1 - f2) . x = (f1 . x) - (f2 . x) & (f1 + (- f2)) . x = (f1 . x) + ((- f2) . x) ) by A42, A44, MESFUNC1:def 3, MESFUNC1:def 4;
hence (f1 - f2) . x = (f1 + (- f2)) . x by A47, MESFUNC1:def 7; :: thesis: verum

end;

hence f1 - f2 = f1 + (- f2) by A42, PARTFUN1:34; :: thesis: verum