let m be Nat; :: thesis: for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L holds
ex L1, L2 being FinSequence st
( L2 is_Finseq_for v & L = L1 ^ L2 & L2 . 1 = L . m & 1 <= len L2 & len L2 = (len L) - (m - 1) & L2 . (len L2) = L . (len L) )
let L be FinSequence; :: thesis: for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L holds
ex L1, L2 being FinSequence st
( L2 is_Finseq_for v & L = L1 ^ L2 & L2 . 1 = L . m & 1 <= len L2 & len L2 = (len L) - (m - 1) & L2 . (len L2) = L . (len L) )
let v be LTL-formula; :: thesis: ( L is_Finseq_for v & 1 <= m & m <= len L implies ex L1, L2 being FinSequence st
( L2 is_Finseq_for v & L = L1 ^ L2 & L2 . 1 = L . m & 1 <= len L2 & len L2 = (len L) - (m - 1) & L2 . (len L2) = L . (len L) ) )
assume that
A1: L is_Finseq_for v and
A2: 1 <= m and
A3: m <= len L ; :: thesis: ex L1, L2 being FinSequence st
( L2 is_Finseq_for v & L = L1 ^ L2 & L2 . 1 = L . m & 1 <= len L2 & len L2 = (len L) - (m - 1) & L2 . (len L2) = L . (len L) )
A4: m - 1 <= (len L) - 0 by A3, XREAL_1:13;
set m1 = m - 1;
reconsider m1 = m - 1 as Nat by A2, NAT_1:21;
set L1 = L | (Seg m1);
reconsider L1 = L | (Seg m1) as FinSequence by FINSEQ_1:15;
consider L2 being FinSequence such that
A5: L = L1 ^ L2 by FINSEQ_1:80;
len L = (len L1) + (len L2) by A5, FINSEQ_1:22;
then A6: len L2 = (len L) - (len L1)
.= (len L) - m1 by A4, FINSEQ_1:17 ;
m - m <= (len L) - m by A3, XREAL_1:9;
then A7: 0 + 1 <= ((len L) - m) + 1 by XREAL_1:6;
then 1 in dom L2 by A6, FINSEQ_3:25;
then A8: L2 . 1 = L . ((len L1) + 1) by A5, FINSEQ_1:def 7
.= L . (m1 + 1) by A4, FINSEQ_1:17
.= L . m ;
A9: len L1 = m1 by A4, FINSEQ_1:17;
for k being Nat st 1 <= k & k < len L2 holds
ex N, M being strict LTLnode over v st
( N = L2 . k & M = L2 . (k + 1) & M is_succ_of N )

proof

let k be Nat; :: thesis: ( 1 <= k & k < len L2 implies ex N, M being strict LTLnode over v st
( N = L2 . k & M = L2 . (k + 1) & M is_succ_of N ) )
assume A10: ( 1 <= k & k < len L2 ) ; :: thesis: ex N, M being strict LTLnode over v st
( N = L2 . k & M = L2 . (k + 1) & M is_succ_of N )
set k1 = k + 1;
( 1 <= k + 1 & k + 1 <= len L2 ) by A10, NAT_1:13;
then A11: k + 1 in dom L2 by FINSEQ_3:25;
set km1 = k + m1;
( 1 + 0 <= k + m1 & k + m1 < ((len L) - m1) + m1 ) by A6, A10, XREAL_1:6, XREAL_1:7;
then consider N, M being strict LTLnode over v such that
A12: N = L . (k + m1) and
A13: M = L . ((k + m1) + 1) and
A14: M is_succ_of N by A1;
A15: M = L . (m1 + (k + 1)) by A13
.= L2 . (k + 1) by A9, A5, A11, FINSEQ_1:def 7 ;
k in dom L2 by A10, FINSEQ_3:25;
then N = L2 . k by A9, A5, A12, FINSEQ_1:def 7;
hence ex N, M being strict LTLnode over v st
( N = L2 . k & M = L2 . (k + 1) & M is_succ_of N ) by A14, A15; :: thesis: verum

end;

then A16: L2 is_Finseq_for v ;
len L2 in dom L2 by A7, A6, FINSEQ_3:25;
then L2 . (len L2) = L . ((len L1) + (len L2)) by A5, FINSEQ_1:def 7
.= L . (len L) by A5, FINSEQ_1:22 ;
hence ex L1, L2 being FinSequence st
( L2 is_Finseq_for v & L = L1 ^ L2 & L2 . 1 = L . m & 1 <= len L2 & len L2 = (len L) - (m - 1) & L2 . (len L2) = L . (len L) ) by A7, A5, A6, A8, A16; :: thesis: verum