:: deftheorem defines TermAlg EQUATION:def 3 :
for S being non empty non void ManySortedSign holds TermAlg S = FreeMSA ( the carrier of S --> NAT);