theorem :: MEASUR11:36

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