:: deftheorem defines CompoundTerm MSATERM:def 6 :
for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for b₃ being Term of S,V holds
( b₃ is CompoundTerm of S,V iff b₃ . {} in [: the carrier' of S,{ the carrier of S}:] );