let MS be non void 1 -element segmental ManySortedSign ; for A, B being non-empty MSAlgebra over 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 over MS; ( 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
; 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 14;
A3:
1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #)
by MSUALG_1:def 14;
the Charact of A =
the charact of (1-Alg A)
by A3, MSUALG_1:def 13
.=
the Charact of B
by A1, A2, MSUALG_1:def 13
;
hence
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
by A4, PBOOLE:3; verum