theorem Th23: :: MEASUR11:29

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