let A1, A2 be strict MSAlgebra of 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

now

let i be set ; :: 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
A7: i = homsym a,b by Th24;
thus the Sorts of A1 . i = Hom a,b by A1, A7
.= the Sorts of A2 . i by A4, A7 ; :: thesis: verum

end;

then A8: the Sorts of A1 = the Sorts of A2 by PBOOLE:3;

now

let i be set ; :: 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 Th25;

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

then consider a being Object of C such that
A9: o = idsym a by Th26;
( the_result_sort_of (idsym a) = homsym a,a & the Sorts of A1 . (homsym a,a) = Hom a,a & the Sorts of A2 . (homsym a,a) = Hom a,a ) by A1, A4, Def5;
then ( Result (idsym a),A1 = Hom a,a & Result (idsym a),A2 = Hom a,a & id a in Hom a,a ) by CAT_1:55, PRALG_2:10;
then A10: ( dom (Den (idsym a),A1) = Args (idsym a),A1 & dom (Den (idsym a),A2) = Args (idsym a),A2 & Args (idsym a),A1 = {{} } & Args (idsym a),A2 = {{} } ) by Th34, FUNCT_2:def 1;

now

let x be set ; :: 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 x = {} by TARSKI:def 1;
then ( (Den (idsym a),A1) . x = id a & (Den (idsym a),A2) . x = id a ) by A2, A5;
hence (Den (idsym a),A1) . x = (Den (idsym a),A2) . x ; :: thesis: verum

end;

hence the Charact of A1 . i = the Charact of A2 . i by A9, A10, FUNCT_1:9; :: 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
A11: o = compsym a,b,c by Th27;
A12: ( Result (compsym a,b,c),A1 = Hom a,c & Result (compsym a,b,c),A2 = Hom a,c & Args (compsym a,b,c),A1 = product <*(Hom b,c),(Hom a,b)*> & Args (compsym a,b,c),A2 = product <*(Hom b,c),(Hom a,b)*> ) by A1, A4, Lm3;

now

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 ;
consider x being Element of X;
consider g, f being set such that
A13: ( g in Hom b,c & f in Hom a,b & x = <*g,f*> ) by FUNCT_6:2;
reconsider g = g, f = f as Morphism of C by A13;
( dom f = a & cod f = b & dom g = b & cod g = c ) by A13, CAT_1:18;
then ( dom (g * f) = a & cod (g * f) = c ) by CAT_1:42;
hence Hom a,c <> {} by CAT_1:18; :: thesis: verum

end;

then A14: ( dom (Den (compsym a,b,c),A1) = Args (compsym a,b,c),A1 & dom (Den (compsym a,b,c),A2) = Args (compsym a,b,c),A2 ) by A12, FUNCT_2:def 1;

now

let x be set ; :: 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 set such that
A15: ( g in Hom b,c & f in Hom a,b & x = <*g,f*> ) by FUNCT_6:2;
reconsider g = g, f = f as Morphism of C by A15;
( dom f = a & cod f = b & dom g = b & cod g = c ) by A15, CAT_1:18;
then ( (Den (compsym a,b,c),A1) . x = g * f & (Den (compsym a,b,c),A2) . x = g * f ) by A3, A6, A15;
hence (Den (compsym a,b,c),A1) . x = (Den (compsym a,b,c),A2) . x ; :: thesis: verum

end;

hence the Charact of A1 . i = the Charact of A2 . i by A11, A12, A14, FUNCT_1:9; :: thesis: verum

end;

end;

end;

hence A1 = A2 by A8, PBOOLE:3; :: thesis: verum