let f, g, h be Function; :: thesis: ( ( for x being object holds
( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being object st x in dom h holds
h . x = g . (f . x) ) implies h = g * f )
assume that
A1: for x being object holds
( x in dom h iff ( x in dom f & f . x in dom g ) ) and
A2: for x being object st x in dom h holds
h . x = g . (f . x) ; :: thesis: h = g * f

now :: thesis: for x, y being object holds
( ( [x,y] in h implies ex y1 being object st
( [x,y1] in f & [y1,y] in g ) ) & ( ex z being object st
( [x,z] in f & [z,y] in g ) implies [x,y] in h ) )

let x, y be object ; :: thesis: ( ( [x,y] in h implies ex y1 being object st
( [x,y1] in f & [y1,y] in g ) ) & ( ex z being object st
( [x,z] in f & [z,y] in g ) implies [x,y] in h ) )

hereby :: thesis: ( ex z being object st
( [x,z] in f & [z,y] in g ) implies [x,y] in h )

assume A3: [x,y] in h ; :: thesis: ex y1 being object st
( [x,y1] in f & [y1,y] in g )
then A4: x in dom h by XTUPLE_0:def 12;
then A5: f . x in dom g by A1;
reconsider y1 = f . x as object ;
take y1 = y1; :: thesis: ( [x,y1] in f & [y1,y] in g )
x in dom f by A1, A4;
hence [x,y1] in f by Def2; :: thesis: [y1,y] in g
reconsider yy = y as set by TARSKI:1;
yy = h . x by A3, A4, Def2
.= g . (f . x) by A2, A4 ;
hence [y1,y] in g by A5, Def2; :: thesis: verum

end;

given z being object such that A6: [x,z] in f and
A7: [z,y] in g ; :: thesis: [x,y] in h
A8: x in dom f by A6, XTUPLE_0:def 12;
reconsider z = z as set by TARSKI:1;
A9: z = f . x by A6, Def2, A8;
A10: z in dom g by A7, XTUPLE_0:def 12;
then A11: x in dom h by A1, A8, A9;
reconsider yy = y as set by TARSKI:1;
yy = g . z by A7, A10, Def2;
then y = h . x by A2, A9, A11;
hence [x,y] in h by A11, Def2; :: thesis: verum

end;

hence h = g * f by RELAT_1:def 8; :: thesis: verum