theorem Th39: :: MEASUR11:45

for X being set
for Y being non empty set
for E being SetSequence of [:X,Y:]
for x being set st E is non-ascending holds
ex G being SetSequence of Y st
( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )