for I being set
for F being ManySortedFunction of I
for Z being ManySortedSet of I st Z is V39() & Z c= rngs F holds
ex Y being ManySortedSet of I st
( Y c= doms F & Y is V39() & F .:.: Y = Z )