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