let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
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))
for x being Element of X1 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = 0 ) holds
(Integral2 (M2,f)) . x = 0
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
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))
for x being Element of X1 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = 0 ) holds
(Integral2 (M2,f)) . x = 0
let S2 be SigmaField of X2; :: 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))
for x being Element of X1 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = 0 ) holds
(Integral2 (M2,f)) . x = 0
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))
for x being Element of X1 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = 0 ) holds
(Integral2 (M2,f)) . x = 0
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = 0 ) holds
(Integral2 (M2,f)) . x = 0
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for x being Element of X1 st A = dom f & ( f is nonnegative or f is nonpositive ) & f is A -measurable & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = 0 ) holds
(Integral2 (M2,f)) . x = 0
let x be Element of X1; :: thesis: ( A = dom f & ( f is nonnegative or f is nonpositive ) & f is A -measurable & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = 0 ) implies (Integral2 (M2,f)) . x = 0 )
assume that
A1: A = dom f and
A2: ( f is nonnegative or f is nonpositive ) and
A3: f is A -measurable and
A4: for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = 0 ; :: thesis: (Integral2 (M2,f)) . x = 0
A5: dom (ProjPMap1 (f,x)) = X-section (A,x) by A1, Def3
.= Measurable-X-section (A,x) by MEASUR11:def 6 ;
A6: ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable by A1, A3, Th47;

per cases ( f is nonnegative or f is nonpositive ) by A2;

suppose A7: f is nonnegative ; :: thesis: (Integral2 (M2,f)) . x = 0

integral+ (M2,(ProjPMap1 (f,x))) = 0 by A1, A3, A4, A5, Th47, MESFUNC5:87;
then Integral (M2,(ProjPMap1 (f,x))) = 0 by A5, A6, A7, Th32, MESFUNC5:88;
hence (Integral2 (M2,f)) . x = 0 by Def8; :: thesis: verum

end;

suppose f is nonpositive ; :: thesis: (Integral2 (M2,f)) . x = 0

then A8: ProjPMap1 (f,x) is nonpositive by Th33;
A9: dom (- (ProjPMap1 (f,x))) = Measurable-X-section (A,x) by A5, MESFUNC1:def 7;
for y being Element of X2 st y in dom (- (ProjPMap1 (f,x))) holds
(- (ProjPMap1 (f,x))) . y = 0

proof

let y be Element of X2; :: thesis: ( y in dom (- (ProjPMap1 (f,x))) implies (- (ProjPMap1 (f,x))) . y = 0 )
assume A10: y in dom (- (ProjPMap1 (f,x))) ; :: thesis: (- (ProjPMap1 (f,x))) . y = 0
then (- (ProjPMap1 (f,x))) . y = - ((ProjPMap1 (f,x)) . y) by MESFUNC1:def 7;
then (- (ProjPMap1 (f,x))) . y = - 0 by A4, A5, A9, A10;
hence (- (ProjPMap1 (f,x))) . y = 0 ; :: thesis: verum

end;

then integral+ (M2,(- (ProjPMap1 (f,x)))) = 0 by A5, A6, A9, MEASUR11:63, MESFUNC5:87;
then - (integral+ (M2,(- (ProjPMap1 (f,x))))) = 0 ;
then Integral (M2,(ProjPMap1 (f,x))) = 0 by A5, A6, A8, MESFUN11:57;
hence (Integral2 (M2,f)) . x = 0 by Def8; :: thesis: verum

end;

end;