theorem Th2: :: FUNCT_6:2

for x being object
for f being Function st x in dom (~ f) holds
ex y, z being object st x = [y,z]