defpred S1[ 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)) & S1[x,y] )
proof
let x be
object ;
( x in Hom ((cod f),(dom g)) implies ex y being object st
( y in Hom ((dom f),(cod g)) & S1[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))
;
ex y being object st
( y in Hom ((dom f),(cod g)) & S1[x,y] )
then reconsider h =
x as
Morphism of
cod f,
dom g by CAT_1:def 5;
take
(g (*) h) (*) f
;
( (g (*) h) (*) f in Hom ((dom f),(cod g)) & S1[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)) &
S1[
x,
(g (*) h) (*) f] )
by A4, A2, CAT_1:23;
verum
end;
consider h being Function such that
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
S1[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
; 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; verum