theorem :: FUNCT_2:123

for X being set
for Y being non empty set
for f being Function of X,Y
for g being b₁ -valued Function holds dom (f * g) = dom g