defpred S_{1}[ object , object ] 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 object st x in the carrier' of C holds

ex y being object st

( y in Maps (Hom C) & S_{1}[x,y] )

A7: ( dom h = the carrier' of C & rng h c= Maps (Hom C) ) and

A8: for x being object st x in the carrier' of C holds

S_{1}[x,h . x]
from FUNCT_1:sch 6(A6);

reconsider h = h as Function of the carrier' of C,(Maps (Hom C)) by A7, FUNCT_2:def 1, RELSET_1:4;

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

$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 object st x in the carrier' of C holds

ex y being object st

( y in Maps (Hom C) & S

proof

consider h being Function such that
let x be object ; :: thesis: ( x in the carrier' of C implies ex y being object st

( y in Maps (Hom C) & S_{1}[x,y] ) )

assume x in the carrier' of C ; :: thesis: ex y being object st

( y in Maps (Hom C) & S_{1}[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_{1}[x,y] )

y is Element of Maps (Hom C) by Th47;

hence ( y in Maps (Hom C) & S_{1}[x,y] )
; :: thesis: verum

end;( y in Maps (Hom C) & S

assume x in the carrier' of C ; :: thesis: ex y being object st

( y in Maps (Hom C) & S

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

y is Element of Maps (Hom C) by Th47;

hence ( y in Maps (Hom C) & S

A7: ( dom h = the carrier' of C & rng h c= Maps (Hom C) ) and

A8: for x being object st x in the carrier' of C holds

S

reconsider h = h as Function of the carrier' of C,(Maps (Hom C)) by A7, FUNCT_2:def 1, RELSET_1:4;

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