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;
A2: f2 " {+infty } = (- f2) " {-infty }

proof

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

end;

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

end;

then (- f2) " {-infty } c= f2 " {+infty } by SUBSET_1:7;
hence f2 " {+infty } = (- f2) " {-infty } by A4, XBOOLE_0:def 10; :: thesis: verum

end;

A7: f2 " {-infty } = (- f2) " {+infty }

proof

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

end;

then A9: 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 x in (- f2) " {+infty } ; :: thesis: x in f2 " {-infty }
then A10: ( x in dom (- f2) & (- f2) . x in {+infty } ) by FUNCT_1:def 13;
then A11: ( x in dom f2 & (- f2) . x = +infty ) by MESFUNC1:def 7, TARSKI:def 1;
then +infty = - (f2 . x) by A10, 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 A11, FUNCT_1:def 13; :: thesis: verum

end;

then (- f2) " {+infty } c= f2 " {-infty } by SUBSET_1:7;
hence f2 " {-infty } = (- f2) " {+infty } by A9, XBOOLE_0:def 10; :: thesis: verum

end;

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 A2, A7, MESFUNC1:def 7 ;
then A12: 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 A13: x in dom (f1 - f2) ; :: thesis: (f1 - f2) . x = (f1 + (- f2)) . x
then A14: (f1 - f2) . x = (f1 . x) - (f2 . x) by MESFUNC1:def 4;
dom (f1 - f2) c= (dom f1) /\ (dom f2) by A1, XBOOLE_1:36;
then ( x in dom f1 & x in dom f2 ) by A13, XBOOLE_0:def 4;
then A15: x in dom (- f2) by MESFUNC1:def 7;
(f1 + (- f2)) . x = (f1 . x) + ((- f2) . x) by A12, A13, MESFUNC1:def 3;
hence (f1 - f2) . x = (f1 + (- f2)) . x by A14, A15, MESFUNC1:def 7; :: thesis: verum

end;

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