theorem Th22: :: MEASUR11:28

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