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 ; :: thesis: ( 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:] ; :: thesis: 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))]; :: thesis: ( y in Maps (Hom C) & S1[x,y] )
y is Element of Maps (Hom C) by Th51;
hence y in Maps (Hom C) ; :: thesis: S1[x,y]
let f9, g9 be Morphism of C; :: thesis: ( x = [f9,g9] implies y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))] )
assume x = [f9,g9] ; :: thesis: y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))]
then ( f9 = f & g9 = g ) by ;
hence y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))] ; :: thesis: 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 reconsider h = h as Function of the carrier' of [:C,C:],(Maps (Hom C)) by ;
take h ; :: thesis: 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; :: thesis: verum