defpred S1[ object , object ] means for f, g being Morphism of C st $1 = [f,g] holds
$2 = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))];
set X = the carrier' of [:C,C:];
set Y = Maps (Hom C);
A1:
for x being object st x in the carrier' of [:C,C:] holds
ex y being object st
( y in Maps (Hom C) & S1[x,y] )
proof
let x be
object ;
( x in the carrier' of [:C,C:] implies ex y being object st
( y in Maps (Hom C) & S1[x,y] ) )
assume
x in the
carrier' of
[:C,C:]
;
ex y being object st
( y in Maps (Hom C) & S1[x,y] )
then consider f,
g being
Morphism of
C such that A2:
x = [f,g]
by DOMAIN_1:1;
take y =
[[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))];
( y in Maps (Hom C) & S1[x,y] )
y is
Element of
Maps (Hom C)
by Th51;
hence
y in Maps (Hom C)
;
S1[x,y]
let f9,
g9 be
Morphism of
C;
( x = [f9,g9] implies y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))] )
assume
x = [f9,g9]
;
y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))]
then
(
f9 = f &
g9 = g )
by A2, XTUPLE_0:1;
hence
y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))]
;
verum
end;
consider h being Function such that
A3:
( dom h = the carrier' of [:C,C:] & rng h c= Maps (Hom C) )
and
A4:
for x being object st x in the carrier' of [:C,C:] holds
S1[x,h . x]
from FUNCT_1:sch 6(A1);
reconsider h = h as Function of the carrier' of [:C,C:],(Maps (Hom C)) by A3, FUNCT_2:def 1, RELSET_1:4;
take
h
; for f, g being Morphism of C holds h . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]
thus
for f, g being Morphism of C holds h . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]
by A4; verum