let f be FinSequence of (TOP-REAL 2); :: 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 A2, FINSEQ_1:59, NAT_1:11;

reconsider k1 = k - 1 as Element of NAT by A1, INT_1:5;

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 A1, FINSEQ_1:1;

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 A5, FINSEQ_1:59;

A12: Seg k1 c= Seg k by A10, FINSEQ_1:5;

L~ ((f | k) | k1) misses LSeg (f,k)

A23: k + 1 = k1 + (1 + 1) ;

1 + 1 <= k by A1, NAT_1:13;

then A24: 1 <= k1 by XREAL_1:19;

then A25: k1 in Seg k by A10, FINSEQ_1:1;

k1 + 1 in Seg k by A1, FINSEQ_1:1;

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 A22, XBOOLE_1:23

.= (LSeg (f,k1)) /\ (LSeg (f,(k1 + 1))) by A6, A7, A25, A5, TOPREAL3:17

.= {(f /. k)} by A2, A3, A24, A23 ;

:: thesis: verum

(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 A2, FINSEQ_1:59, NAT_1:11;

reconsider k1 = k - 1 as Element of NAT by A1, INT_1:5;

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 A1, FINSEQ_1:1;

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 A5, FINSEQ_1:59;

A12: Seg k1 c= Seg k by A10, FINSEQ_1:5;

L~ ((f | k) | k1) misses LSeg (f,k)

proof

then A22:
(L~ ((f | k) | k1)) /\ (LSeg (f,k)) = {}
;
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 A13, TARSKI:def 4;

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 A18, A19, SEQ_4:134;

then LSeg (((f | k) | k1),n) = LSeg ((f | k),n) by TOPREAL3:17;

then LSeg (((f | k) | k1),n) = LSeg (f,n) by A6, A12, A8, A5, A11, A20, TOPREAL3:17;

then A21: LSeg (f,n) meets LSeg (f,k) by A14, A15, A17, XBOOLE_0:3;

n + 1 < k by A9, A11, A19, XXREAL_0:2;

hence contradiction by A4, A21; :: thesis: verum

end;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 A13, TARSKI:def 4;

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 A18, A19, SEQ_4:134;

then LSeg (((f | k) | k1),n) = LSeg ((f | k),n) by TOPREAL3:17;

then LSeg (((f | k) | k1),n) = LSeg (f,n) by A6, A12, A8, A5, A11, A20, TOPREAL3:17;

then A21: LSeg (f,n) meets LSeg (f,k) by A14, A15, A17, XBOOLE_0:3;

n + 1 < k by A9, A11, A19, XXREAL_0:2;

hence contradiction by A4, A21; :: thesis: verum

A23: k + 1 = k1 + (1 + 1) ;

1 + 1 <= k by A1, NAT_1:13;

then A24: 1 <= k1 by XREAL_1:19;

then A25: k1 in Seg k by A10, FINSEQ_1:1;

k1 + 1 in Seg k by A1, FINSEQ_1:1;

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 A22, XBOOLE_1:23

.= (LSeg (f,k1)) /\ (LSeg (f,(k1 + 1))) by A6, A7, A25, A5, TOPREAL3:17

.= {(f /. k)} by A2, A3, A24, A23 ;

:: thesis: verum