:: deftheorem Def10 defines finitely-generated MSAFREE2:def 10 :
for S being non empty ManySortedSign
for IT being MSAlgebra over S holds
( ( not S is void implies ( IT is finitely-generated iff for S9 being non empty non void ManySortedSign st S9 = S holds
for A being MSAlgebra over S9 st A = IT holds
ex G being GeneratorSet of A st G is V39() ) ) & ( S is void implies ( IT is finitely-generated iff the Sorts of IT is V39() ) ) );