theorem Th18: :: FUNCT_6:22

for x being object
for g being Function
for f being Function-yielding Function st x in dom f & g = f . x holds
( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) by Def1, Def2;