theorem Th17: :: AOFA_000:17

for X being non empty disjoint_with_NAT set
for S being non empty FinSequence of NAT
for i being Nat st i in dom S holds
for p being FinSequence of (FreeUnivAlgNSG (S,X)) st len p = S . i holds
(Den ((In (i,(dom the charact of (FreeUnivAlgNSG (S,X))))),(FreeUnivAlgNSG (S,X)))) . p = i -tree p