theorem :: MEASUR11:37

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