let k be Nat; :: thesis: for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= k & k < len L holds
CastNode (L . (k + 1)),v is_succ_of CastNode (L . k),v
let L be FinSequence; :: thesis: for v being LTL-formula st L is_Finseq_for v & 1 <= k & k < len L holds
CastNode (L . (k + 1)),v is_succ_of CastNode (L . k),v
let v be LTL-formula; :: thesis: ( L is_Finseq_for v & 1 <= k & k < len L implies CastNode (L . (k + 1)),v is_succ_of CastNode (L . k),v )
assume ( L is_Finseq_for v & 1 <= k & k < len L ) ; :: thesis: CastNode (L . (k + 1)),v is_succ_of CastNode (L . k),v
then consider N, M being strict LTLnode of v such that
A1: N = L . k and
A2: ( M = L . (k + 1) & M is_succ_of N ) by Def19;
CastNode (L . k),v = N by A1, Def16;
hence CastNode (L . (k + 1)),v is_succ_of CastNode (L . k),v by A2, Def16; :: thesis: verum