theorem Th12: :: LTLAXIO2:12

for f being FinSequence of LTLB_WFF
for k, n being Nat st n <= k holds
(con f) . n = (con (f | k)) . n