let MS be non empty trivial non void segmental ManySortedSign ; :: thesis: for A, B being non-empty MSAlgebra of MS st 1-Alg A = 1-Alg B holds
MSAlgebra(# the Sorts of A,the Charact of A #) = MSAlgebra(# the Sorts of B,the Charact of B #)
let A, B be non-empty MSAlgebra of MS; :: thesis: ( 1-Alg A = 1-Alg B implies MSAlgebra(# the Sorts of A,the Charact of A #) = MSAlgebra(# the Sorts of B,the Charact of B #) )
assume A1: 1-Alg A = 1-Alg B ; :: thesis: MSAlgebra(# the Sorts of A,the Charact of A #) = MSAlgebra(# the Sorts of B,the Charact of B #)
A2: 1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #) by MSUALG_1:def 19;
A3: 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def 19;

A4: now

let i be set ; :: thesis: ( i in the carrier of MS implies the Sorts of A . i = the Sorts of B . i )
assume A5: i in the carrier of MS ; :: thesis: the Sorts of A . i = the Sorts of B . i
A6: ex c being Component of the Sorts of B st the Sorts of B . i = c

proof

reconsider c = the Sorts of B . i as Component of the Sorts of B by A5, PBOOLE:151;
take c ; :: thesis: the Sorts of B . i = c
thus the Sorts of B . i = c ; :: thesis: verum

end;

ex c being Component of the Sorts of A st the Sorts of A . i = c

proof

reconsider c = the Sorts of A . i as Component of the Sorts of A by A5, PBOOLE:151;
take c ; :: thesis: the Sorts of A . i = c
thus the Sorts of A . i = c ; :: thesis: verum

end;

then the Sorts of A . i = the_sort_of B by A1, A3, A2, MSUALG_1:def 17
.= the Sorts of B . i by A6, MSUALG_1:def 17 ;
hence the Sorts of A . i = the Sorts of B . i ; :: thesis: verum

end;

the Charact of A = the charact of (1-Alg A) by A3, MSUALG_1:def 18
.= the Charact of B by A1, A2, MSUALG_1:def 18 ;
hence MSAlgebra(# the Sorts of A,the Charact of A #) = MSAlgebra(# the Sorts of B,the Charact of B #) by A4, PBOOLE:3; :: thesis: verum