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

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