let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
let U0 be MSAlgebra over S; :: thesis: for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
let U1, U2 be MSSubAlgebra of U0; :: thesis: ( the Sorts of U1 = the Sorts of U2 implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
assume the Sorts of U1 = the Sorts of U2 ; :: thesis: MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
then ( U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 ) by Th8;
hence MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by Th7; :: thesis: verum