deffunc H₁( Object of C) -> Morphism of $1,$1 = id $1;
deffunc H₂( Object of C, Object of C, Object of C, Morphism of C, Morphism of C) -> Element of the carrier' of C = $4 (*) $5;
deffunc H₃( Object of C, Object of C) -> Element of bool the carrier' of C = Hom ($1,$2);
A31: for a being Object of C holds H₁(a) in H₃(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 H₃(a,b) & g in H₃(b,c) holds
H₂(a,b,c,g,f) in H₃(a,c)

let a, b, c be Object of C; :: thesis: for f, g being Morphism of C st f in H₃(a,b) & g in H₃(b,c) holds
H₂(a,b,c,g,f) in H₃(a,c)
let f, g be Morphism of C; :: thesis: ( f in H₃(a,b) & g in H₃(b,c) implies H₂(a,b,c,g,f) in H₃(a,c) )
assume that
A33: f in H₃(a,b) and
A34: g in H₃(b,c) ; :: thesis: H₂(a,b,c,g,f) in H₃(a,c)
A35: ( cod f = b & dom g = b ) by A33, A34, CAT_1:1;
cod g = c by A34, CAT_1:1;
then A36: cod (g (*) f) = c by A35, CAT_1:17;
dom f = a by A33, CAT_1:1;
then dom (g (*) f) = a by A35, CAT_1:17;
hence H₂(a,b,c,g,f) in H₃(a,c) by A36; :: thesis: verum

end;

A37: for a, b being Object of C holds H₃(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)) = H₃(a,b) ) & ( for a being Element of C holds (Den ((idsym a),A)) . {} = H₁(a) ) ) and
A39: for a, b, c being Element of C
for f, g being Element of the carrier' of C st f in H₃(a,b) & g in H₃(b,c) holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = H₂(a,b,c,g,f) from CATALG_1:sch 1(A37, A31, A32);
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 ((idsym a),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 ((idsym a),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