theorem Th33: :: AOFA_A00:38

for S being non empty non void ManySortedSign
for A, B being non-empty 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
for H being GeneratorSet of B st G = H & G is free holds
H is free