let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2)) st E = dom f & f is E -measurable holds
( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2)) st E = dom f & f is E -measurable holds
( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2)) st E = dom f & f is E -measurable holds
( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2)) st E = dom f & f is E -measurable holds
( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )
let M2 be sigma_Measure of S2; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2)) st E = dom f & f is E -measurable holds
( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2)) st E = dom f & f is E -measurable holds
( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( A = dom f & f is A -measurable implies ( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) ) )
assume that
A1: A = dom f and
A2: f is A -measurable ; :: thesis: ( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )
A3: ( dom (- (Integral1 (M1,f))) = X2 & dom (- (Integral2 (M2,f))) = X1 ) by FUNCT_2:def 1;

now :: thesis: for y being Element of X2 holds (Integral1 (M1,(- f))) . y = (- (Integral1 (M1,f))) . y

let y be Element of X2; :: thesis: (Integral1 (M1,(- f))) . y = (- (Integral1 (M1,f))) . y
ProjPMap2 ((- f),y) = ProjPMap2 (((- 1) (#) f),y) by MESFUNC2:9
.= (- 1) (#) (ProjPMap2 (f,y)) by Th29
.= - (ProjPMap2 (f,y)) by MESFUNC2:9 ;
then A4: (Integral1 (M1,(- f))) . y = Integral (M1,(- (ProjPMap2 (f,y)))) by Def7;
dom (ProjPMap2 (f,y)) = Y-section (A,y) by A1, Def4;
then A5: dom (ProjPMap2 (f,y)) = Measurable-Y-section (A,y) by MEASUR11:def 7;
(- (Integral1 (M1,f))) . y = - ((Integral1 (M1,f)) . y) by A3, MESFUNC1:def 7;
then (- (Integral1 (M1,f))) . y = - (Integral (M1,(ProjPMap2 (f,y)))) by Def7;
hence (Integral1 (M1,(- f))) . y = (- (Integral1 (M1,f))) . y by A1, A2, A4, A5, Th47, MESFUN11:52; :: thesis: verum

end;

hence Integral1 (M1,(- f)) = - (Integral1 (M1,f)) by FUNCT_2:def 8; :: thesis: Integral2 (M2,(- f)) = - (Integral2 (M2,f))

now :: thesis: for x being Element of X1 holds (Integral2 (M2,(- f))) . x = (- (Integral2 (M2,f))) . x

let x be Element of X1; :: thesis: (Integral2 (M2,(- f))) . x = (- (Integral2 (M2,f))) . x
ProjPMap1 ((- f),x) = ProjPMap1 (((- 1) (#) f),x) by MESFUNC2:9
.= (- 1) (#) (ProjPMap1 (f,x)) by Th29
.= - (ProjPMap1 (f,x)) by MESFUNC2:9 ;
then A6: (Integral2 (M2,(- f))) . x = Integral (M2,(- (ProjPMap1 (f,x)))) by Def8;
dom (ProjPMap1 (f,x)) = X-section (A,x) by A1, Def3;
then A7: dom (ProjPMap1 (f,x)) = Measurable-X-section (A,x) by MEASUR11:def 6;
(- (Integral2 (M2,f))) . x = - ((Integral2 (M2,f)) . x) by A3, MESFUNC1:def 7;
then (- (Integral2 (M2,f))) . x = - (Integral (M2,(ProjPMap1 (f,x)))) by Def8;
hence (Integral2 (M2,(- f))) . x = (- (Integral2 (M2,f))) . x by A1, A2, A6, A7, Th47, MESFUN11:52; :: thesis: verum

end;

hence Integral2 (M2,(- f)) = - (Integral2 (M2,f)) by FUNCT_2:def 8; :: thesis: verum