:: deftheorem defines free MSAFREE:def 5 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for IT being GeneratorSet of U0 holds
( IT is free iff for U1 being non-empty MSAlgebra over S
for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st
( h is_homomorphism U0,U1 & h || IT = f ) );