:: deftheorem Def2 defines con LTLAXIO2:def 2 :
for f, b₂ being FinSequence of LTLB_WFF holds
( ( len f > 0 implies ( b₂ = con f iff ( len b₂ = len f & b₂ . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₂ . (i + 1) = (b₂ /. i) '&&' (f /. (i + 1)) ) ) ) ) & ( not len f > 0 implies ( b₂ = con f iff b₂ = <*TVERUM*> ) ) );