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;

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

hence
A1 = A2
by A1, A2, PBOOLE:3; :: thesis: verumthe 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;

end;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

hence
the Charact of A1 . i = the Charact of A2 . i
by FUNCT_2:12; :: thesis: verumf1 . 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;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