theorem Th67: :: AOFA_000:67

for X being non empty disjoint_with_NAT set
for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 4 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
ex C, I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*C,I*>