theorem Th1: :: WAYBEL27:1

for X, Y, Z, D being set st D c= Funcs (X,(Funcs (Y,Z))) holds
ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) )