let S be non empty non void ManySortedSign ; :: thesis: for A, B being MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for G being GeneratorSet of A holds G is GeneratorSet of B
let A, B be MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) implies for G being GeneratorSet of A holds G is GeneratorSet of B )
assume A1: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ; :: thesis: for G being GeneratorSet of A holds G is GeneratorSet of B
let G be GeneratorSet of A; :: thesis: G is GeneratorSet of B
reconsider H = G as MSSubset of B by A1;
GenMSAlg H = GenMSAlg G by A1, Th31;
hence G is GeneratorSet of B by A1, MSAFREE:def 4; :: thesis: verum