let f be FinSequence of (); :: thesis: for k being Nat st 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. holds
(L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)}

let k be Nat; :: thesis: ( 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. implies (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)} )
assume that
A1: 1 < k and
A2: len f = k + 1 and
A3: f is unfolded and
A4: f is s.n.c. ; :: thesis: (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)}
set f1 = f | k;
A5: len (f | k) = k by ;
reconsider k1 = k - 1 as Element of NAT by ;
set f2 = (f | k) | k1;
set l2 = { (LSeg (((f | k) | k1),m)) where m is Nat : ( 1 <= m & m + 1 <= len ((f | k) | k1) ) } ;
A6: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def 3;
A7: k in Seg k by ;
A8: dom ((f | k) | k1) = Seg (len ((f | k) | k1)) by FINSEQ_1:def 3;
A9: k1 < k by XREAL_1:44;
A10: k1 <= k by XREAL_1:44;
then A11: len ((f | k) | k1) = k1 by ;
A12: Seg k1 c= Seg k by ;
L~ ((f | k) | k1) misses LSeg (f,k)
proof
assume not L~ ((f | k) | k1) misses LSeg (f,k) ; :: thesis: contradiction
then consider x being object such that
A13: x in L~ ((f | k) | k1) and
A14: x in LSeg (f,k) by XBOOLE_0:3;
consider X being set such that
A15: x in X and
A16: X in { (LSeg (((f | k) | k1),m)) where m is Nat : ( 1 <= m & m + 1 <= len ((f | k) | k1) ) } by ;
consider n being Nat such that
A17: X = LSeg (((f | k) | k1),n) and
A18: 1 <= n and
A19: n + 1 <= len ((f | k) | k1) by A16;
A20: ( n in dom ((f | k) | k1) & n + 1 in dom ((f | k) | k1) ) by ;
then LSeg (((f | k) | k1),n) = LSeg ((f | k),n) by TOPREAL3:17;
then LSeg (((f | k) | k1),n) = LSeg (f,n) by ;
then A21: LSeg (f,n) meets LSeg (f,k) by ;
n + 1 < k by ;
hence contradiction by A4, A21; :: thesis: verum
end;
then A22: (L~ ((f | k) | k1)) /\ (LSeg (f,k)) = {} ;
A23: k + 1 = k1 + (1 + 1) ;
1 + 1 <= k by ;
then A24: 1 <= k1 by XREAL_1:19;
then A25: k1 in Seg k by ;
k1 + 1 in Seg k by ;
then L~ (f | k) = (L~ ((f | k) | k1)) \/ (LSeg ((f | k),k1)) by A24, A5, Th3;
hence (L~ (f | k)) /\ (LSeg (f,k)) = {} \/ ((LSeg ((f | k),k1)) /\ (LSeg (f,k))) by
.= (LSeg (f,k1)) /\ (LSeg (f,(k1 + 1))) by
.= {(f /. k)} by A2, A3, A24, A23 ;
:: thesis: verum