defpred S₁[ object , object ] 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 object st x in Hom ((cod f),a) holds
ex y being object st
( y in Hom ((dom f),a) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Hom ((cod f),a) implies ex y being object st
( y in Hom ((dom f),a) & S₁[x,y] ) )
assume A9: x in Hom ((cod f),a) ; :: thesis: ex y being object st
( y in Hom ((dom f),a) & S₁[x,y] )
then reconsider g = x as Morphism of cod f,a by CAT_1:def 5;
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:2, CAT_1:4;
hence ( g (*) f in Hom ((dom f),a) & S₁[x,g (*) f] ) by A9, CAT_1:23; :: 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 object st x in Hom ((cod f),a) holds
S₁[x,h . x] from FUNCT_1:sch 6(A8);
Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;
then reconsider h = h as Function of (Hom ((cod f),a)),(Hom ((dom f),a)) by A10, FUNCT_2:def 1, RELSET_1:4;
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