let A1, A2 be strict MSAlgebra over S; :: thesis: ( the Sorts of A1 = the carrier of S --> {0} & the Sorts of A2 = the carrier of S --> {0} implies A1 = A2 )
assume that
A1: the Sorts of A1 = the carrier of S --> {0} and
A2: the Sorts of A2 = the carrier of S --> {0} ; :: thesis: A1 = A2
set B = the Sorts of A1;
A3: 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 A4: i in the carrier' of S ; :: thesis: the Charact of A1 . i = the Charact of A2 . i
then A5: ( the Sorts of A1 * the ResultSort of S) . i = the Sorts of A1 . ( the ResultSort of S . i) by A3, FUNCT_1:13
.= {0} by A1, A4, FUNCOP_1:7, 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 A1, A2, A4, 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 A6: 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 A7: f1 . x = 0 by A5, TARSKI:def 1;
f2 . x in A by A6, FUNCT_2:5;
hence f1 . x = f2 . x by A5, A7, 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 A1, A2, PBOOLE:3; :: thesis: verum