theorem Th22: :: MSAFREE5:50

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( deg t <> 0 iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )