theorem Th11: :: FUNCT_1:11

for x being object
for f, g being Function holds
( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )