defpred S1[ object , object ] means for f being Morphism of C st f = \$1 holds
\$2 = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))];
set X = the carrier' of C;
set Y = Maps (Hom C);
A1: for x being object st x in the carrier' of C holds
ex y being object st
( y in Maps (Hom C) & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier' of C implies ex y being object st
( y in Maps (Hom C) & S1[x,y] ) )

assume x in the carrier' of C ; :: thesis: ex y being object st
( y in Maps (Hom C) & S1[x,y] )

then reconsider f = x as Morphism of C ;
take y = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]; :: thesis: ( y in Maps (Hom C) & S1[x,y] )
y is Element of Maps (Hom C) by Th46;
hence ( y in Maps (Hom C) & S1[x,y] ) ; :: thesis: verum
end;
consider h being Function such that
A2: ( dom h = the carrier' of C & rng h c= Maps (Hom C) ) and
A3: for x being object st x in the carrier' of C holds
S1[x,h . x] from reconsider h = h as Function of the carrier' of C,(Maps (Hom C)) by ;
take h ; :: thesis: for f being Morphism of C holds h . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]
thus for f being Morphism of C holds h . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] by A3; :: thesis: verum