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

now

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

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

assume A3: [x,y] in h ; :: thesis: ex y1 being set st
( [x,y1] in f & [y1,y] in g )
then A4: x in dom h by RELAT_1:def 4;
then A5: f . x in dom g by A1;
take y1 = f . x; :: thesis: ( [x,y1] in f & [y1,y] in g )
x in dom f by A1, A4;
hence [x,y1] in f by Def4; :: thesis: [y1,y] in g
y = h . x by A3, A4, Def4
.= g . (f . x) by A2, A4 ;
hence [y1,y] in g by A5, Def4; :: thesis: verum

end;

given z being set 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, RELAT_1:def 4;
then A9: z = f . x by A6, Def4;
A10: z in dom g by A7, RELAT_1:def 4;
then A11: x in dom h by A1, A8, A9;
y = g . z by A7, A10, Def4;
then y = h . x by A2, A9, A11;
hence [x,y] in h by A11, Def4; :: thesis: verum

end;

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