theorem Th2: :: WAYBEL27:2

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