let x be object ; :: thesis: for f, g being Function holds
( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )
let f, g be Function; :: thesis: ( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )
set h = g * f;

hereby :: thesis: ( x in dom f & f . x in dom g implies x in dom (g * f) )

assume x in dom (g * f) ; :: thesis: ( x in dom f & f . x in dom g )
then consider y being object such that
A1: [x,y] in g * f by XTUPLE_0:def 12;
consider z being object such that
A2: [x,z] in f and
A3: [z,y] in g by A1, RELAT_1:def 8;
reconsider z = z as set by TARSKI:1;
thus x in dom f by A2, XTUPLE_0:def 12; :: thesis: f . x in dom g
then z = f . x by A2, Def2;
hence f . x in dom g by A3, XTUPLE_0:def 12; :: thesis: verum

end;

assume A4: x in dom f ; :: thesis: ( not f . x in dom g or x in dom (g * f) )
then consider z being object such that
A5: [x,z] in f by XTUPLE_0:def 12;
assume f . x in dom g ; :: thesis: x in dom (g * f)
then consider y being object such that
A6: [(f . x),y] in g by XTUPLE_0:def 12;
reconsider z = z as set by TARSKI:1;
z = f . x by A4, A5, Def2;
then [x,y] in g * f by A5, A6, RELAT_1:def 8;
hence x in dom (g * f) by XTUPLE_0:def 12; :: thesis: verum