theorem Th3: :: FUNCT_3:3

for X being set
for f, g being Function st X c= dom f & f .: X c= dom g holds
X c= dom (g * f)