theorem Th30: :: FUNCT_5:37

for X, Y being set
for f being Function st rng f c= PFuncs (X,Y) holds
( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] )