theorem Th38: :: MEASUR11:44

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