:: deftheorem defines -free MSAFREE4:def 12 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for T being EqualSet of S
for G being GeneratorSet of A holds
( G is T -free iff for B being non-empty b₃ -satisfying MSAlgebra over S
for f being ManySortedFunction of G, the Sorts of B ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & h || G = f ) );