theorem Th8: :: LTLAXIO2:8

for f being FinSequence of LTLB_WFF
for i being Nat st i in dom f holds
(nega f) /. i = 'not' (f /. i)