theorem :: FUNCT_6:33

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