deffunc H1( Object of C) -> Morphism of \$1,\$1 = id \$1;
deffunc H2( Object of C, Object of C, Object of C, Morphism of C, Morphism of C) -> Element of the carrier' of C = \$4 (*) \$5;
deffunc H3( Object of C, Object of C) -> Element of bool the carrier' of C = Hom (\$1,\$2);
A31: for a being Object of C holds H1(a) in H3(a,a) by CAT_1:27;
A32: now :: thesis: for a, b, c being Object of C
for f, g being Morphism of C st f in H3(a,b) & g in H3(b,c) holds
H2(a,b,c,g,f) in H3(a,c)
let a, b, c be Object of C; :: thesis: for f, g being Morphism of C st f in H3(a,b) & g in H3(b,c) holds
H2(a,b,c,g,f) in H3(a,c)

let f, g be Morphism of C; :: thesis: ( f in H3(a,b) & g in H3(b,c) implies H2(a,b,c,g,f) in H3(a,c) )
assume that
A33: f in H3(a,b) and
A34: g in H3(b,c) ; :: thesis: H2(a,b,c,g,f) in H3(a,c)
A35: ( cod f = b & dom g = b ) by ;
cod g = c by ;
then A36: cod (g (*) f) = c by ;
dom f = a by ;
then dom (g (*) f) = a by ;
hence H2(a,b,c,g,f) in H3(a,c) by A36; :: thesis: verum
end;
A37: for a, b being Object of C holds H3(a,b) c= the carrier' of C ;
consider A being strict MSAlgebra over CatSign the carrier of C such that
A38: ( ( for a, b being Element of C holds the Sorts of A . (homsym (a,b)) = H3(a,b) ) & ( for a being Element of C holds (Den ((),A)) . {} = H1(a) ) ) and
A39: for a, b, c being Element of C
for f, g being Element of the carrier' of C st f in H3(a,b) & g in H3(b,c) holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = H2(a,b,c,g,f) from take A ; :: thesis: ( ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((),A)) . {} = id a ) & ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f ) )

now :: thesis: for a, b, c being Object of C
for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f
let a, b, c be Object of C; :: thesis: for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f

let f, g be Morphism of C; :: thesis: ( dom f = a & cod f = b & dom g = b & cod g = c implies (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f )
assume ( dom f = a & cod f = b & dom g = b & cod g = c ) ; :: thesis: (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f
then ( f in Hom (a,b) & g in Hom (b,c) ) ;
hence (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f by A39; :: thesis: verum
end;
hence ( ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((),A)) . {} = id a ) & ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f ) ) by A38; :: thesis: verum