let A1, A2 be strict MSAlgebra over S; :: thesis: ( ( for i being set st i in the carrier of S holds
the Sorts of A1 . i = {i} ) & ( for i being set st i in the carrier of S holds
the Sorts of A2 . i = {i} ) implies A1 = A2 )
assume that
A2: for i being set st i in the carrier of S holds
the Sorts of A1 . i = {i} and
A3: for i being set st i in the carrier of S holds
the Sorts of A2 . i = {i} ; :: thesis: A1 = A2
set B = the Sorts of A1;

now :: thesis: for i being object st i in the carrier of S holds
the Sorts of A1 . i = the Sorts of A2 . i

let i be object ; :: thesis: ( i in the carrier of S implies the Sorts of A1 . i = the Sorts of A2 . i )
assume A4: i in the carrier of S ; :: thesis: the Sorts of A1 . i = the Sorts of A2 . i
hence the Sorts of A1 . i = {i} by A2
.= the Sorts of A2 . i by A3, A4 ;
:: thesis: verum

end;

then A5: the Sorts of A1 = the Sorts of A2 ;
A6: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

now :: thesis: for i being object st i in the carrier' of S holds
the Charact of A1 . i = the Charact of A2 . i

let i be object ; :: thesis: ( i in the carrier' of S implies the Charact of A1 . i = the Charact of A2 . i )
set A = ( the Sorts of A1 * the ResultSort of S) . i;
assume A7: i in the carrier' of S ; :: thesis: the Charact of A1 . i = the Charact of A2 . i
then A8: ( the Sorts of A1 * the ResultSort of S) . i = the Sorts of A1 . ( the ResultSort of S . i) by A6, FUNCT_1:13
.= {( the ResultSort of S . i)} by A2, A7, FUNCT_2:5 ;
then reconsider A = ( the Sorts of A1 * the ResultSort of S) . i as non empty set ;
reconsider f1 = the Charact of A1 . i, f2 = the Charact of A2 . i as Function of ((( the Sorts of A1 #) * the Arity of S) . i),A by A5, A7, PBOOLE:def 15;

now :: thesis: for x being object st x in (( the Sorts of A1 #) * the Arity of S) . i holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in (( the Sorts of A1 #) * the Arity of S) . i implies f1 . x = f2 . x )
assume A9: x in (( the Sorts of A1 #) * the Arity of S) . i ; :: thesis: f1 . x = f2 . x
then f1 . x in A by FUNCT_2:5;
then A10: f1 . x = the ResultSort of S . i by A8, TARSKI:def 1;
f2 . x in A by A9, FUNCT_2:5;
hence f1 . x = f2 . x by A8, A10, TARSKI:def 1; :: thesis: verum

end;

hence the Charact of A1 . i = the Charact of A2 . i by FUNCT_2:12; :: thesis: verum

end;

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