let f be FinSequence of LTLB_WFF ; :: thesis: for i being Nat st i in dom f holds
(nex f) /. i = 'X' (f /. i)
let i be Nat; :: thesis: ( i in dom f implies (nex f) /. i = 'X' (f /. i) )
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
assume A1: i in dom f ; :: thesis: (nex f) /. i = 'X' (f /. i)
then A2: 1 <= i by FINSEQ_3:25;
A3: i <= len f by A1, FINSEQ_3:25;
then i <= len (nex f) by Def5;
hence (nex f) /. i = (nex f) . i1 by A2, FINSEQ_4:15
.= 'X' (f /. i) by Def5, A2, A3 ;
:: thesis: verum