theorem Th19: :: LTLAXIO2:19

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