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

proof

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

end;

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