theorem Th27: :: FUNCT_6:32

for x being object
for f being Function-yielding Function st x in dom <:f:> holds
for g being Function st g in rng f holds
x in dom g