theorem Th7: :: LTLAXIO2:7

for f being FinSequence of LTLB_WFF
for i being Nat st 1 <= i & i < len f holds
(con f) /. (i + 1) = ((con f) /. i) '&&' (f /. (i + 1))