defpred S_{1}[ 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) & S_{1}[x,y] )

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

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

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

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

$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) & S

proof

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

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

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

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

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

hence y in Maps (Hom C) ; :: thesis: S_{1}[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 A2, XTUPLE_0:1;

hence y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))] ; :: thesis: verum

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

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

( y in Maps (Hom C) & S

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) & S

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

hence y in Maps (Hom C) ; :: thesis: S

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 A2, XTUPLE_0:1;

hence y = [[(Hom ((cod f9),(dom g9))),(Hom ((dom f9),(cod g9)))],(hom (f9,g9))] ; :: thesis: verum

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

S

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

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