defpred S_{1}[ object , object ] means for h being Morphism of C st h = $1 holds

$2 = (g (*) h) (*) f;

set X = Hom ((cod f),(dom g));

set Y = Hom ((dom f),(cod g));

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

ex y being object st

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

A5: ( dom h = Hom ((cod f),(dom g)) & rng h c= Hom ((dom f),(cod g)) ) and

A6: for x being object st x in Hom ((cod f),(dom g)) holds

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

( Hom ((dom f),(cod g)) = {} implies Hom ((cod f),(dom g)) = {} ) by Th50;

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

take h ; :: thesis: for h being Morphism of C st h in Hom ((cod f),(dom g)) holds

h . h = (g (*) h) (*) f

thus for h being Morphism of C st h in Hom ((cod f),(dom g)) holds

h . h = (g (*) h) (*) f by A6; :: thesis: verum

$2 = (g (*) h) (*) f;

set X = Hom ((cod f),(dom g));

set Y = Hom ((dom f),(cod g));

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

ex y being object st

( y in Hom ((dom f),(cod g)) & S

proof

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

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

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

assume A3: x in Hom ((cod f),(dom g)) ; :: thesis: ex y being object st

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

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

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

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

then A4: g (*) h in Hom ((cod f),(cod g)) by A3, CAT_1:23;

then g (*) h is Morphism of cod f, cod g by CAT_1:def 5;

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

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

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

assume A3: x in Hom ((cod f),(dom g)) ; :: thesis: ex y being object st

( y in Hom ((dom f),(cod g)) & S

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

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

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

then A4: g (*) h in Hom ((cod f),(cod g)) by A3, CAT_1:23;

then g (*) h is Morphism of cod f, cod g by CAT_1:def 5;

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

A5: ( dom h = Hom ((cod f),(dom g)) & rng h c= Hom ((dom f),(cod g)) ) and

A6: for x being object st x in Hom ((cod f),(dom g)) holds

S

( Hom ((dom f),(cod g)) = {} implies Hom ((cod f),(dom g)) = {} ) by Th50;

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

take h ; :: thesis: for h being Morphism of C st h in Hom ((cod f),(dom g)) holds

h . h = (g (*) h) (*) f

thus for h being Morphism of C st h in Hom ((cod f),(dom g)) holds

h . h = (g (*) h) (*) f by A6; :: thesis: verum