let f be FinSequence of (TOP-REAL 2); for k being Element of 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 Element of NAT ; ( 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.
; (L~ (f | k)) /\ (LSeg f,k) = {(f /. k)}
set f1 = f | k;
A5:
len (f | k) = k
by A2, FINSEQ_1:80, NAT_1:11;
reconsider k1 = k - 1 as Element of NAT by A1, INT_1:18;
set f2 = (f | k) | k1;
set l2 = { (LSeg ((f | k) | k1),m) where m is Element of 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:3;
A8:
dom ((f | k) | k1) = Seg (len ((f | k) | k1))
by FINSEQ_1:def 3;
A9:
k1 < k
by XREAL_1:46;
A10:
k1 <= k
by XREAL_1:46;
then A11:
len ((f | k) | k1) = k1
by A5, FINSEQ_1:80;
A12:
Seg k1 c= Seg k
by A10, FINSEQ_1:7;
L~ ((f | k) | k1) misses LSeg f,k
proof
assume
not
L~ ((f | k) | k1) misses LSeg f,
k
;
contradiction
then consider x being
set 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 Element of NAT : ( 1 <= m & m + 1 <= len ((f | k) | k1) ) }
by A13, TARSKI:def 4;
consider n being
Element of
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:151;
then
LSeg ((f | k) | k1),
n = LSeg (f | k),
n
by TOPREAL3:24;
then
LSeg ((f | k) | k1),
n = LSeg f,
n
by A6, A12, A8, A5, A11, A20, TOPREAL3:24;
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, TOPREAL1:def 9;
verum
end;
then A22:
(L~ ((f | k) | k1)) /\ (LSeg f,k) = {}
by XBOOLE_0:def 7;
A23:
k + 1 = k1 + (1 + 1)
;
1 + 1 <= k
by A1, NAT_1:13;
then A24:
1 <= k1
by XREAL_1:21;
then A25:
k1 in Seg k
by A10, FINSEQ_1:3;
k1 + 1 in Seg k
by A1, FINSEQ_1:3;
then
L~ (f | k) = (L~ ((f | k) | k1)) \/ (LSeg (f | k),k1)
by A24, A5, Th8;
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:24
.=
{(f /. k)}
by A2, A3, A24, A23, TOPREAL1:def 8
;
verum