theorem Th26: :: MEASUR11:32

for X being non empty set
for Y, p being set
for F being SetSequence of [:X,Y:]
for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds
Y-section ((union (rng F)),p) = union (rng Fx)