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

let i be set ; :: 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:23
.= {0 } by A1, A4, FUNCOP_1:13, FUNCT_2:7 ;
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 18;

now

let x be set ; :: thesis: ( x in ((the Sorts of A1 # ) * the Arity of S) . i implies f1 . x = f2 . x )
assume x in ((the Sorts of A1 # ) * the Arity of S) . i ; :: thesis: f1 . x = f2 . x
then ( f1 . x in A & f2 . x in A ) by FUNCT_2:7;
then ( f1 . x = 0 & f2 . x = 0 ) by A5, TARSKI:def 1;
hence f1 . x = f2 . x ; :: thesis: verum

end;

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

end;

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