for X1, X2 being non empty set
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 E, E1, E2 being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & E1 misses E2 holds
( Integral1 (M1,(f | (E1 \/ E2))) = (Integral1 (M1,(f | E1))) + (Integral1 (M1,(f | E2))) & Integral2 (M2,(f | (E1 \/ E2))) = (Integral2 (M2,(f | E1))) + (Integral2 (M2,(f | E2))) ) by Lm11, Lm12;