let X be non empty set ; :: thesis: for f being Function of X,X
for g being X -valued Function holds dom (f * g) = dom g
let f be Function of X,X; :: 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 by RELAT_1:def 19;
hence dom (f * g) = dom g by RELAT_1:46; :: thesis: verum