theorem :: MEASUR11:37

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