let A1, A2 be strict MSAlgebra over S; :: thesis: ( the Sorts of A1 = the carrier of S --> & the Sorts of A2 = the carrier of S --> implies A1 = A2 )
assume that
A1: the Sorts of A1 = the carrier of S --> and
A2: the Sorts of A2 = the carrier of S --> ; :: 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
.= by ;
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 ;
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 ;
f2 . x in A by ;
hence f1 . x = f2 . x by ; :: 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 ; :: thesis: verum