let x be set ; :: thesis: for g, f being Function holds
( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )
let g, f 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 set such that
A1: [x,y] in g * f by RELAT_1:def 4;
consider z being set such that
A2: [x,z] in f and
A3: [z,y] in g by A1, RELAT_1:def 8;
thus x in dom f by A2, RELAT_1:def 4; :: thesis: f . x in dom g
then z = f . x by A2, Def4;
hence f . x in dom g by A3, RELAT_1:def 4; :: 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 set such that
A5: [x,z] in f by RELAT_1:def 4;
assume f . x in dom g ; :: thesis: x in dom (g * f)
then consider y being set such that
A6: [(f . x),y] in g by RELAT_1:def 4;
z = f . x by A4, A5, Def4;
then [x,y] in g * f by A5, A6, RELAT_1:def 8;
hence x in dom (g * f) by RELAT_1:def 4; :: thesis: verum