deffunc H₁( Object of C, Object of C) -> Element of bool the carrier' of C = Hom $1,$2;
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) -> Morphism of $1,$1 = id $1;
A16: for a, b being Object of C holds H₁(a,b) c= the carrier' of C ;
A17: for a being Object of C holds H₃(a) in H₁(a,a) by CAT_1:55;

A18: now

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 ( f in H₁(a,b) & g in H₁(b,c) ) ; :: thesis: H₂(a,b,c,g,f) in H₁(a,c)
then ( dom f = a & cod f = b & dom g = b & cod g = c ) by CAT_1:18;
then ( dom (g * f) = a & cod (g * f) = c ) by CAT_1:42;
hence H₂(a,b,c,g,f) in H₁(a,c) by CAT_1:18; :: thesis: verum

end;

consider A being strict MSAlgebra of CatSign the carrier of C such that
A19: for a, b being Element of the carrier of C holds the Sorts of A . (homsym a,b) = H₁(a,b) and
A20: for a being Element of the carrier of C holds (Den (idsym a),A) . {} = H₃(a) and
A21: for a, b, c being Element of the carrier 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(A16, A17, A18);
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

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 ) by CAT_1:18;
hence (Den (compsym a,b,c),A) . <*g,f*> = g * f by A21; :: 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 A19, A20; :: thesis: verum