defpred S1[ 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) & S1[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) & S1[x,y] ) )

assume A9: x in Hom ((cod f),a) ; :: thesis: ex y being object st
( y in Hom ((dom f),a) & S1[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) & S1[x,g (*) f] )
( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by ;
hence ( g (*) f in Hom ((dom f),a) & S1[x,g (*) f] ) by ; :: 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
S1[x,h . x] from 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 ;
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