let A1, A2 be strict MSAlgebra over CatSign the carrier of C; :: thesis: ( ( for a, b being Object of C holds the Sorts of A1 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A1)) . {} = 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)),A1)) . <*g,f*> = g (*) f ) & ( for a, b being Object of C holds the Sorts of A2 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A2)) . {} = 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)),A2)) . <*g,f*> = g (*) f ) implies A1 = A2 )
assume that
A1: for a, b being Object of C holds the Sorts of A1 . (homsym (a,b)) = Hom (a,b) and
A2: for a being Object of C holds (Den ((idsym a),A1)) . {} = id a and
A3: 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)),A1)) . <*g,f*> = g (*) f and
A4: for a, b being Object of C holds the Sorts of A2 . (homsym (a,b)) = Hom (a,b) and
A5: for a being Object of C holds (Den ((idsym a),A2)) . {} = id a and
A6: 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)),A2)) . <*g,f*> = g (*) f ; :: thesis: A1 = A2

A7: now :: thesis: for i being object st i in the carrier' of (CatSign the carrier of C) holds
the Charact of A1 . i = the Charact of A2 . i

let i be object ; :: thesis: ( i in the carrier' of (CatSign the carrier of C) implies the Charact of A1 . b₁ = the Charact of A2 . b₁ )
assume i in the carrier' of (CatSign the carrier of C) ; :: thesis: the Charact of A1 . b₁ = the Charact of A2 . b₁
then reconsider o = i as OperSymbol of (CatSign the carrier of C) ;

per cases ( o `1 = 1 or o `1 = 2 ) by Th16;

suppose o `1 = 1 ; :: thesis: the Charact of A1 . b₁ = the Charact of A2 . b₁

then consider a being Object of C such that
A8: o = idsym a by Th17;
A9: id a in Hom (a,a) by CAT_1:27;
A10: the_result_sort_of (idsym a) = homsym (a,a) by Def3;
the Sorts of A1 . (homsym (a,a)) = Hom (a,a) by A1;
then Result ((idsym a),A1) = Hom (a,a) by A10, PRALG_2:3;
then A11: dom (Den ((idsym a),A1)) = Args ((idsym a),A1) by A9, FUNCT_2:def 1;

A12: now :: thesis: for x being object st x in {{}} holds
(Den ((idsym a),A1)) . x = (Den ((idsym a),A2)) . x

let x be object ; :: thesis: ( x in {{}} implies (Den ((idsym a),A1)) . x = (Den ((idsym a),A2)) . x )
assume x in {{}} ; :: thesis: (Den ((idsym a),A1)) . x = (Den ((idsym a),A2)) . x
then A13: x = {} by TARSKI:def 1;
then (Den ((idsym a),A1)) . x = id a by A2;
hence (Den ((idsym a),A1)) . x = (Den ((idsym a),A2)) . x by A5, A13; :: thesis: verum

end;

the Sorts of A2 . (homsym (a,a)) = Hom (a,a) by A4;
then Result ((idsym a),A2) = Hom (a,a) by A10, PRALG_2:3;
then A14: dom (Den ((idsym a),A2)) = Args ((idsym a),A2) by A9, FUNCT_2:def 1;
( Args ((idsym a),A1) = {{}} & Args ((idsym a),A2) = {{}} ) by Th25;
hence the Charact of A1 . i = the Charact of A2 . i by A8, A11, A14, A12, FUNCT_1:2; :: thesis: verum

end;

suppose o `1 = 2 ; :: thesis: the Charact of A1 . b₁ = the Charact of A2 . b₁

then consider a, b, c being Object of C such that
A15: o = compsym (a,b,c) by Th18;

A16: now :: thesis: ( product <*(Hom (b,c)),(Hom (a,b))*> <> {} implies Hom (a,c) <> {} )

assume product <*(Hom (b,c)),(Hom (a,b))*> <> {} ; :: thesis: Hom (a,c) <> {}
then reconsider X = product <*(Hom (b,c)),(Hom (a,b))*> as non empty set ;
set x = the Element of X;
consider g, f being object such that
A17: g in Hom (b,c) and
A18: f in Hom (a,b) and
the Element of X = <*g,f*> by FINSEQ_3:124;
reconsider g = g, f = f as Morphism of C by A17, A18;
A19: ( cod f = b & dom g = b ) by A17, A18, CAT_1:1;
cod g = c by A17, CAT_1:1;
then A20: cod (g (*) f) = c by A19, CAT_1:17;
dom f = a by A18, CAT_1:1;
then dom (g (*) f) = a by A19, CAT_1:17;
hence Hom (a,c) <> {} by A20, CAT_1:1; :: thesis: verum

end;

A21: now :: thesis: for x being object st x in product <*(Hom (b,c)),(Hom (a,b))*> holds
(Den ((compsym (a,b,c)),A1)) . x = (Den ((compsym (a,b,c)),A2)) . x

let x be object ; :: thesis: ( x in product <*(Hom (b,c)),(Hom (a,b))*> implies (Den ((compsym (a,b,c)),A1)) . x = (Den ((compsym (a,b,c)),A2)) . x )
assume x in product <*(Hom (b,c)),(Hom (a,b))*> ; :: thesis: (Den ((compsym (a,b,c)),A1)) . x = (Den ((compsym (a,b,c)),A2)) . x
then consider g, f being object such that
A22: g in Hom (b,c) and
A23: f in Hom (a,b) and
A24: x = <*g,f*> by FINSEQ_3:124;
reconsider g = g, f = f as Morphism of C by A22, A23;
A25: ( dom g = b & cod g = c ) by A22, CAT_1:1;
A26: ( dom f = a & cod f = b ) by A23, CAT_1:1;
then (Den ((compsym (a,b,c)),A1)) . x = g (*) f by A3, A24, A25;
hence (Den ((compsym (a,b,c)),A1)) . x = (Den ((compsym (a,b,c)),A2)) . x by A6, A24, A26, A25; :: thesis: verum

end;

A27: Args ((compsym (a,b,c)),A1) = product <*(Hom (b,c)),(Hom (a,b))*> by A1, Lm5;
A28: Args ((compsym (a,b,c)),A2) = product <*(Hom (b,c)),(Hom (a,b))*> by A4, Lm5;
Result ((compsym (a,b,c)),A2) = Hom (a,c) by A4, Lm5;
then A29: dom (Den ((compsym (a,b,c)),A2)) = Args ((compsym (a,b,c)),A2) by A28, A16, FUNCT_2:def 1;
Result ((compsym (a,b,c)),A1) = Hom (a,c) by A1, Lm5;
then dom (Den ((compsym (a,b,c)),A1)) = Args ((compsym (a,b,c)),A1) by A27, A16, FUNCT_2:def 1;
hence the Charact of A1 . i = the Charact of A2 . i by A15, A27, A28, A29, A21, FUNCT_1:2; :: thesis: verum

end;

end;

end;

now :: thesis: for i being object st i in the carrier of (CatSign the carrier of C) holds
the Sorts of A1 . i = the Sorts of A2 . i

let i be object ; :: thesis: ( i in the carrier of (CatSign the carrier of C) implies the Sorts of A1 . i = the Sorts of A2 . i )
assume i in the carrier of (CatSign the carrier of C) ; :: thesis: the Sorts of A1 . i = the Sorts of A2 . i
then consider a, b being Object of C such that
A30: i = homsym (a,b) by Th15;
thus the Sorts of A1 . i = Hom (a,b) by A1, A30
.= the Sorts of A2 . i by A4, A30 ; :: thesis: verum

end;

then the Sorts of A1 = the Sorts of A2 ;
hence A1 = A2 by A7, PBOOLE:3; :: thesis: verum