defpred S_{1}[ object , object ] 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 object st x in Hom (a,(dom f)) holds

ex y being object st

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

A3: ( dom h = Hom (a,(dom f)) & rng h c= Hom (a,(cod f)) ) and

A4: for x being object st x in Hom (a,(dom f)) holds

S_{1}[x,h . x]
from FUNCT_1:sch 6(A1);

Hom ((dom f),(cod f)) <> {} by CAT_1:2;

then ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;

then reconsider h = h as Function of (Hom (a,(dom f))),(Hom (a,(cod f))) by A3, FUNCT_2:def 1, RELSET_1:4;

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

$2 = f (*) g;

set X = Hom (a,(dom f));

set Y = Hom (a,(cod f));

A1: for x being object st x in Hom (a,(dom f)) holds

ex y being object st

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

proof

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

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

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

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

then reconsider g = x as Morphism of a, dom f by CAT_1:def 5;

take f (*) g ; :: thesis: ( f (*) g in Hom (a,(cod f)) & S_{1}[x,f (*) g] )

( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by CAT_1:1, CAT_1:4;

hence ( f (*) g in Hom (a,(cod f)) & S_{1}[x,f (*) g] )
by A2, CAT_1:23; :: thesis: verum

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

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

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

then reconsider g = x as Morphism of a, dom f by CAT_1:def 5;

take f (*) g ; :: thesis: ( f (*) g in Hom (a,(cod f)) & S

( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by CAT_1:1, CAT_1:4;

hence ( f (*) g in Hom (a,(cod f)) & S

A3: ( dom h = Hom (a,(dom f)) & rng h c= Hom (a,(cod f)) ) and

A4: for x being object st x in Hom (a,(dom f)) holds

S

Hom ((dom f),(cod f)) <> {} by CAT_1:2;

then ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;

then reconsider h = h as Function of (Hom (a,(dom f))),(Hom (a,(cod f))) by A3, FUNCT_2:def 1, RELSET_1:4;

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