theorem :: MEASUR11:51

for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for Fx being FinSequence of S1
for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = Measurable-Y-section ((F . n),p) ) holds
Measurable-Y-section ((Union F),p) = Union Fx