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 f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = 0 ) holds
(Integral1 (M1,f)) . y = 0
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = 0 ) holds
(Integral1 (M1,f)) . y = 0
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = 0 ) holds
(Integral1 (M1,f)) . y = 0
let M1 be sigma_Measure of S1; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = 0 ) holds
(Integral1 (M1,f)) . y = 0
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = 0 ) holds
(Integral1 (M1,f)) . y = 0
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for y being Element of X2 st A = dom f & ( f is nonnegative or f is nonpositive ) & f is A -measurable & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = 0 ) holds
(Integral1 (M1,f)) . y = 0
let y be Element of X2; :: thesis: ( A = dom f & ( f is nonnegative or f is nonpositive ) & f is A -measurable & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = 0 ) implies (Integral1 (M1,f)) . y = 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 x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = 0 ; :: thesis: (Integral1 (M1,f)) . y = 0
A5: dom (ProjPMap2 (f,y)) = Y-section (A,y) by A1, Def4
.= Measurable-Y-section (A,y) by MEASUR11:def 7 ;
A6: ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable by A1, A3, Th47;

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

suppose A7: f is nonnegative ; :: thesis: (Integral1 (M1,f)) . y = 0

integral+ (M1,(ProjPMap2 (f,y))) = 0 by A1, A3, A4, A5, Th47, MESFUNC5:87;
then Integral (M1,(ProjPMap2 (f,y))) = 0 by A5, A6, A7, Th32, MESFUNC5:88;
hence (Integral1 (M1,f)) . y = 0 by Def7; :: thesis: verum

end;

suppose f is nonpositive ; :: thesis: (Integral1 (M1,f)) . y = 0

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

proof

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

end;

then integral+ (M1,(- (ProjPMap2 (f,y)))) = 0 by A5, A6, A9, MEASUR11:63, MESFUNC5:87;
then - (integral+ (M1,(- (ProjPMap2 (f,y))))) = 0 ;
then Integral (M1,(ProjPMap2 (f,y))) = 0 by A5, A6, A8, MESFUN11:57;
hence (Integral1 (M1,f)) . y = 0 by Def7; :: thesis: verum

end;

end;