:: deftheorem Def1 defines Free MSAFREE3:def 1 :
for S being non void Signature
for X being ManySortedSet of the carrier of S
for b₃ being strict MSAlgebra over S holds
( b₃ = Free (S,X) iff ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st
( b₃ = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) );