let f be FinSequence of LTLB_WFF ; :: thesis: for i being Nat st 1 <= i & i < len f holds
(con f) /. (i + 1) = ((con f) /. i) '&&' (f /. (i + 1))
let i be Nat; :: thesis: ( 1 <= i & i < len f implies (con f) /. (i + 1) = ((con f) /. i) '&&' (f /. (i + 1)) )
assume that
A1: 1 <= i and
A2: i < len f ; :: thesis: (con f) /. (i + 1) = ((con f) /. i) '&&' (f /. (i + 1))
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
i < len (con f) by A2, Def2;
then i + 1 <= len (con f) by NAT_1:13;
hence (con f) /. (i + 1) = (con f) . (i1 + 1) by FINSEQ_4:15, NAT_1:12
.= ((con f) /. i) '&&' (f /. (i + 1)) by Def2, A1, A2 ;
:: thesis: verum