defpred S₁[ set , set ] means for f, g being Morphism of 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 set st x in the carrier' of [:C,C:] holds
ex y being set st
( y in Maps (Hom C) & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the carrier' of [:C,C:] implies ex y being set st
( y in Maps (Hom C) & S₁[x,y] ) )
assume x in the carrier' of [:C,C:] ; :: thesis: ex y being set st
( y in Maps (Hom C) & S₁[x,y] )
then consider f, g being Morphism of such that
A2: x = [f,g] by DOMAIN_1:9;
take y = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)]; :: thesis: ( y in Maps (Hom C) & S₁[x,y] )
y is Element of Maps (Hom C) by Th52;
hence y in Maps (Hom C) ; :: thesis: S₁[x,y]
let f', g' be Morphism of ; :: thesis: ( x = [f',g'] implies y = [[(Hom (cod f'),(dom g')),(Hom (dom f'),(cod g'))],(hom f',g')] )
assume x = [f',g'] ; :: thesis: y = [[(Hom (cod f'),(dom g')),(Hom (dom f'),(cod g'))],(hom f',g')]
then ( f' = f & g' = g ) by A2, ZFMISC_1:33;
hence y = [[(Hom (cod f'),(dom g')),(Hom (dom f'),(cod g'))],(hom f',g')] ; :: 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 set st x in the carrier' of [:C,C:] holds
S₁[x,h . x] from WELLORD2:sch 1(A1);
reconsider h = h as Function of the carrier' of [:C,C:], Maps (Hom C) by A3, FUNCT_2:def 1, RELSET_1:11;
take h ; :: thesis: for f, g being Morphism of holds h . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)]
thus for f, g being Morphism of holds h . [f,g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] by A4; :: thesis: verum