theorem Th20: :: LTLAXIO2:20

for f being FinSequence of LTLB_WFF
for g being Function of LTLB_WFF,BOOLEAN holds
( (VAL g) . ('not' ((con (nega f)) /. (len (con (nega f))))) = 0 iff for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 0 )