deffunc H_{1}( Object of C) -> Morphism of $1,$1 = id $1;

deffunc H_{2}( 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_{3}( 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_{1}(a) in H_{3}(a,a)
by CAT_1:27;

_{3}(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_{3}(a,b) ) & ( for a being Element of C holds (Den ((idsym a),A)) . {} = H_{1}(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_{3}(a,b) & g in H_{3}(b,c) holds

(Den ((compsym (a,b,c)),A)) . <*g,f*> = H_{2}(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 ) )

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

deffunc H

deffunc H

A31: for a being Object of C holds H

A32: now :: thesis: for a, b, c being Object of C

for f, g being Morphism of C st f in H_{3}(a,b) & g in H_{3}(b,c) holds

H_{2}(a,b,c,g,f) in H_{3}(a,c)

A37:
for a, b being Object of C holds Hfor f, g being Morphism of C st f in H

H

let a, b, c be Object of C; :: thesis: for f, g being Morphism of C st f in H_{3}(a,b) & g in H_{3}(b,c) holds

H_{2}(a,b,c,g,f) in H_{3}(a,c)

let f, g be Morphism of C; :: thesis: ( f in H_{3}(a,b) & g in H_{3}(b,c) implies H_{2}(a,b,c,g,f) in H_{3}(a,c) )

assume that

A33: f in H_{3}(a,b)
and

A34: g in H_{3}(b,c)
; :: thesis: H_{2}(a,b,c,g,f) in H_{3}(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_{2}(a,b,c,g,f) in H_{3}(a,c)
by A36; :: thesis: verum

end;H

let f, g be Morphism of C; :: thesis: ( f in H

assume that

A33: f in H

A34: g in H

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

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

A39: for a, b, c being Element of C

for f, g being Element of the carrier' of C st f in H

(Den ((compsym (a,b,c)),A)) . <*g,f*> = H

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

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 Cfor 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;(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

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