defpred S_{1}[ 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_{1}[x,y] )

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_{1}[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

$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

proof

consider h being Function such that
let x be object ; :: thesis: ( x in Hom ((cod f),a) implies ex y being object st

( y in Hom ((dom f),a) & S_{1}[x,y] ) )

assume A9: x in Hom ((cod f),a) ; :: thesis: ex y being object st

( y in Hom ((dom f),a) & S_{1}[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_{1}[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_{1}[x,g (*) f] )
by A9, CAT_1:23; :: thesis: verum

end;( y in Hom ((dom f),a) & S

assume A9: x in Hom ((cod f),a) ; :: thesis: ex y being object st

( y in Hom ((dom f),a) & S

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

( 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

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

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