let f, g be Function; :: thesis: dom (f * g) = (dom g) /\ (g " (dom f))
thus dom (f * g) c= (dom g) /\ (g " (dom f)) :: according to XBOOLE_0:def 10 :: thesis: (dom g) /\ (g " (dom f)) c= dom (f * g)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f * g) or x in (dom g) /\ (g " (dom f)) )
assume A1: x in dom (f * g) ; :: thesis: x in (dom g) /\ (g " (dom f))
then A2: x in dom g by FUNCT_1:11;
g . x in dom f by A1, FUNCT_1:11;
then x in g " (dom f) by A2, FUNCT_1:def 7;
hence x in (dom g) /\ (g " (dom f)) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom g) /\ (g " (dom f)) or x in dom (f * g) )
assume A3: x in (dom g) /\ (g " (dom f)) ; :: thesis: x in dom (f * g)
then x in g " (dom f) by XBOOLE_0:def 4;
then A4: g . x in dom f by FUNCT_1:def 7;
x in dom g by A3, XBOOLE_0:def 4;
hence x in dom (f * g) by A4, FUNCT_1:11; :: thesis: verum