theorem :: MEASUR11:50

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 Fy being FinSequence of S2
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Measurable-X-section ((F . n),p) ) holds
Measurable-X-section ((Union F),p) = Union Fy