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

end;

A10: f2 " {+infty } c= (- f2) " {-infty } by A2, SUBSET_1:7;
A11: 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 }
A13: x in dom (- f2) by A12, 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;
A16: (- f2) . x = -infty by A14, TARSKI:def 1;
A17: -infty = - (f2 . x) by A13, A16, MESFUNC1:def 7;
A18: f2 . x in {+infty } by A17, TARSKI:def 1, XXREAL_3:5;
thus x in f2 " {+infty } by A15, A18, FUNCT_1:def 13; :: thesis: verum

end;

A19: (- f2) " {-infty } c= f2 " {+infty } by A11, SUBSET_1:7;
A20: f2 " {+infty } = (- f2) " {-infty } by A10, A19, XBOOLE_0:def 10;
A21: 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 }
A23: x in dom f2 by A22, 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;
A26: f2 . x = -infty by A24, TARSKI:def 1;
A27: (- f2) . x = +infty by A25, A26, MESFUNC1:def 7, XXREAL_3:5;
A28: (- f2) . x in {+infty } by A27, TARSKI:def 1;
thus x in (- f2) " {+infty } by A25, A28, FUNCT_1:def 13; :: thesis: verum

end;

A29: f2 " {-infty } c= (- f2) " {+infty } by A21, SUBSET_1:7;
A30: 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 }
A32: x in dom (- f2) by A31, 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;
A35: (- f2) . x = +infty by A33, TARSKI:def 1;
A36: +infty = - (f2 . x) by A32, A35, MESFUNC1:def 7;
A37: f2 . x = - +infty by A36
.= -infty by XXREAL_3:def 3 ;
A38: f2 . x in {-infty } by A37, TARSKI:def 1;
thus x in f2 " {-infty } by A34, A38, FUNCT_1:def 13; :: thesis: verum

end;

A39: (- f2) " {+infty } c= f2 " {-infty } by A30, SUBSET_1:7;
A40: f2 " {-infty } = (- f2) " {+infty } by A29, A39, XBOOLE_0:def 10;
A41: 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 ;
A42: dom (f1 - f2) = dom (f1 + (- f2)) by A41, MESFUNC1:def 4;
A43: 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
A45: dom (f1 - f2) c= (dom f1) /\ (dom f2) by A1, XBOOLE_1:36;
A46: x in dom f2 by A44, A45, XBOOLE_0:def 4;
A47: x in dom (- f2) by A46, MESFUNC1:def 7;
A48: ( (f1 - f2) . x = (f1 . x) - (f2 . x) & (f1 + (- f2)) . x = (f1 . x) + ((- f2) . x) ) by A42, A44, MESFUNC1:def 3, MESFUNC1:def 4;
thus (f1 - f2) . x = (f1 + (- f2)) . x by A47, A48, MESFUNC1:def 7; :: thesis: verum

end;

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