defpred S₁[ set , set ] means for f being Morphism of C st f = $1 holds
$2 = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)];
set X = the carrier' of C;
set Y = Maps (Hom C);
A6: for x being set st x in the carrier' of 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 implies ex y being set st
( y in Maps (Hom C) & S₁[x,y] ) )
assume x in the carrier' of C ; :: thesis: ex y being set st
( y in Maps (Hom C) & S₁[x,y] )
then reconsider f = x as Morphism of C ;
take y = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)]; :: thesis: ( y in Maps (Hom C) & S₁[x,y] )
y is Element of Maps (Hom C) by Th48;
hence ( y in Maps (Hom C) & S₁[x,y] ) ; :: thesis: verum

end;

consider h being Function such that
A7: ( dom h = the carrier' of C & rng h c= Maps (Hom C) ) and
A8: for x being set st x in the carrier' of C holds
S₁[x,h . x] from WELLORD2:sch 1(A6);
reconsider h = h as Function of the carrier' of C,(Maps (Hom C)) by A7, FUNCT_2:def 1, RELSET_1:11;
take h ; :: thesis: for f being Morphism of C holds h . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)]
thus for f being Morphism of C holds h . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] by A8; :: thesis: verum