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 A2: x in f2 " {+infty} ; :: thesis: x in (- f2) " {-infty}
then A3: x in dom f2 by FUNCT_1:def 7;
A4: f2 . x in {+infty} by A2, FUNCT_1:def 7;
A5: x in dom (- f2) by A3, MESFUNC1:def 7;
f2 . x = +infty by A4, TARSKI:def 1;
then (- f2) . x = - +infty by A5, MESFUNC1:def 7
.= -infty by XXREAL_3:def 3 ;
then (- f2) . x in {-infty} by TARSKI:def 1;
hence x in (- f2) " {-infty} by A5, FUNCT_1:def 7; :: thesis: verum

end;

then A6: f2 " {+infty} c= (- f2) " {-infty} ;
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 A7: x in (- f2) " {-infty} ; :: thesis: x in f2 " {+infty}
then A8: x in dom (- f2) by FUNCT_1:def 7;
A9: (- f2) . x in {-infty} by A7, FUNCT_1:def 7;
A10: x in dom f2 by A8, MESFUNC1:def 7;
(- f2) . x = -infty by A9, TARSKI:def 1;
then -infty = - (f2 . x) by A8, MESFUNC1:def 7;
then f2 . x in {+infty} by TARSKI:def 1, XXREAL_3:5;
hence x in f2 " {+infty} by A10, FUNCT_1:def 7; :: thesis: verum

end;

then (- f2) " {-infty} c= f2 " {+infty} ;
then A11: f2 " {+infty} = (- f2) " {-infty} by A6;
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 7;
A14: f2 . x in {-infty} by A12, FUNCT_1:def 7;
A15: x in dom (- f2) by A13, MESFUNC1:def 7;
f2 . x = -infty by A14, TARSKI:def 1;
then (- f2) . x = +infty by A15, MESFUNC1:def 7, XXREAL_3:5;
then (- f2) . x in {+infty} by TARSKI:def 1;
hence x in (- f2) " {+infty} by A15, FUNCT_1:def 7; :: thesis: verum

end;

then A16: f2 " {-infty} c= (- f2) " {+infty} ;
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 A17: x in (- f2) " {+infty} ; :: thesis: x in f2 " {-infty}
then A18: x in dom (- f2) by FUNCT_1:def 7;
A19: (- f2) . x in {+infty} by A17, FUNCT_1:def 7;
A20: x in dom f2 by A18, MESFUNC1:def 7;
(- f2) . x = +infty by A19, TARSKI:def 1;
then +infty = - (f2 . x) by A18, 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 A20, FUNCT_1:def 7; :: thesis: verum

end;

then (- f2) " {+infty} c= f2 " {-infty} ;
then A21: f2 " {-infty} = (- f2) " {+infty} by A16;
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 A11, A21, MESFUNC1:def 7 ;
then A22: 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 A23: 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 A23, XBOOLE_0:def 4;
then A24: x in dom (- f2) by MESFUNC1:def 7;
( (f1 - f2) . x = (f1 . x) - (f2 . x) & (f1 + (- f2)) . x = (f1 . x) + ((- f2) . x) ) by A22, A23, MESFUNC1:def 3, MESFUNC1:def 4;
hence (f1 - f2) . x = (f1 + (- f2)) . x by A24, MESFUNC1:def 7; :: thesis: verum

end;

hence f1 - f2 = f1 + (- f2) by A22, PARTFUN1:5; :: thesis: verum