theorem Th6: :: LTLAXIO4:6

for M being LTLModel
for n being Element of NAT
for f being FinSequence of LTLB_WFF holds
( (SAT M) . [n,((con f) /. (len (con f)))] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )