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;