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

proof

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

end;

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