let X be set ; :: thesis: for Y being non empty set
for f being Function of X,Y
for g being X -valued Function holds dom (f * g) = dom g
let Y be non empty set ; :: thesis: for f being Function of X,Y
for g being X -valued Function holds dom (f * g) = dom g
let f be Function of X,Y; :: thesis: for g being X -valued Function holds dom (f * g) = dom g
let g be X -valued Function; :: thesis: dom (f * g) = dom g
dom f = X by Def1;
then rng g c= dom f ;
hence dom (f * g) = dom g by RELAT_1:27; :: thesis: verum