defpred S₁[ set , set ] means for h being Morphism of C st h = $1 holds
$2 = (g * h) * f;
set X = Hom (cod f),(dom g);
set Y = Hom (dom f),(cod g);
A1: for x being set st x in Hom (cod f),(dom g) holds
ex y being set st
( y in Hom (dom f),(cod g) & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in Hom (cod f),(dom g) implies ex y being set st
( y in Hom (dom f),(cod g) & S₁[x,y] ) )
A2: ( Hom (dom f),(cod f) <> {} & f is Morphism of dom f, cod f ) by CAT_1:19, CAT_1:22;
assume A3: x in Hom (cod f),(dom g) ; :: thesis: ex y being set st
( y in Hom (dom f),(cod g) & S₁[x,y] )
then reconsider h = x as Morphism of cod f, dom g by CAT_1:def 7;
take (g * h) * f ; :: thesis: ( (g * h) * f in Hom (dom f),(cod g) & S₁[x,(g * h) * f] )
( Hom (dom g),(cod g) <> {} & g is Morphism of dom g, cod g ) by CAT_1:19, CAT_1:22;
then A4: g * h in Hom (cod f),(cod g) by A3, CAT_1:51;
then g * h is Morphism of cod f, cod g by CAT_1:def 7;
hence ( (g * h) * f in Hom (dom f),(cod g) & S₁[x,(g * h) * f] ) by A4, A2, CAT_1:51; :: thesis: verum

end;

consider h being Function such that
A5: ( dom h = Hom (cod f),(dom g) & rng h c= Hom (dom f),(cod g) ) and
A6: for x being set st x in Hom (cod f),(dom g) holds
S₁[x,h . x] from WELLORD2:sch 1(A1);
( Hom (dom f),(cod g) = {} implies Hom (cod f),(dom g) = {} ) by Th51;
then reconsider h = h as Function of (Hom (cod f),(dom g)),(Hom (dom f),(cod g)) by A5, FUNCT_2:def 1, RELSET_1:11;
take h ; :: thesis: for h being Morphism of C st h in Hom (cod f),(dom g) holds
h . h = (g * h) * f
thus for h being Morphism of C st h in Hom (cod f),(dom g) holds
h . h = (g * h) * f by A6; :: thesis: verum