let f be FinSequence of (TOP-REAL 2); for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds
(L~ (f -: q)) /\ (L~ (f :- q)) = {q}
let q be Point of (TOP-REAL 2); ( q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. implies (L~ (f -: q)) /\ (L~ (f :- q)) = {q} )
assume that
A1:
q in rng f
and
A2:
1 <> q .. f
and
A3:
q .. f <> len f
and
A4:
f is unfolded
and
A5:
f is s.n.c.
; (L~ (f -: q)) /\ (L~ (f :- q)) = {q}
A6:
(f :- q) /. 1 = q
by FINSEQ_5:53;
q .. f <= len f
by A1, FINSEQ_4:21;
then
q .. f < len f
by A3, XXREAL_0:1;
then
(q .. f) + 1 <= len f
by NAT_1:13;
then A7:
1 <= (len f) - (q .. f)
by XREAL_1:19;
len (f :- q) = ((len f) - (q .. f)) + 1
by A1, FINSEQ_5:50;
then
1 + 1 <= len (f :- q)
by A7, XREAL_1:6;
then A8:
rng (f :- q) c= L~ (f :- q)
by Th18;
1 in dom (f :- q)
by FINSEQ_5:6;
then A9:
q in rng (f :- q)
by A6, PARTFUN2:2;
not f -: q is empty
by A1, FINSEQ_5:47;
then A10:
len (f -: q) in dom (f -: q)
by FINSEQ_5:6;
A11:
len (f -: q) = q .. f
by A1, FINSEQ_5:42;
thus
(L~ (f -: q)) /\ (L~ (f :- q)) c= {q}
XBOOLE_0:def 10 {q} c= (L~ (f -: q)) /\ (L~ (f :- q))proof
let x be
object ;
TARSKI:def 3 ( not x in (L~ (f -: q)) /\ (L~ (f :- q)) or x in {q} )
assume A12:
x in (L~ (f -: q)) /\ (L~ (f :- q))
;
x in {q}
then reconsider p =
x as
Point of
(TOP-REAL 2) ;
p in L~ (f -: q)
by A12, XBOOLE_0:def 4;
then consider i being
Nat such that A13:
1
<= i
and A14:
i + 1
<= len (f -: q)
and A15:
p in LSeg (
(f -: q),
i)
by Th13;
A16:
LSeg (
(f -: q),
i)
= LSeg (
f,
i)
by A14, Th9;
p in L~ (f :- q)
by A12, XBOOLE_0:def 4;
then consider j being
Nat such that A17:
1
<= j
and
j + 1
<= len (f :- q)
and A18:
p in LSeg (
(f :- q),
j)
by Th13;
consider j9 being
Nat such that A19:
j = j9 + 1
by A17, NAT_1:6;
reconsider j9 =
j9 as
Element of
NAT by ORDINAL1:def 12;
A20:
LSeg (
(f :- q),
j)
= LSeg (
f,
(j9 + (q .. f)))
by A1, A19, Th10;
per cases
( ( i + 1 = len (f -: q) & j9 = 0 ) or ( i + 1 = len (f -: q) & j9 <> 0 ) or i + 1 <> len (f -: q) )
;
suppose that A21:
i + 1
= len (f -: q)
and A22:
j9 = 0
;
x in {q}
q .. f <= len f
by A1, FINSEQ_4:21;
then
q .. f < len f
by A3, XXREAL_0:1;
then
(i + 1) + 1
<= len f
by A11, A21, NAT_1:13;
then
i + (1 + 1) <= len f
;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) =
{(f /. (q .. f))}
by A4, A11, A13, A16, A20, A21, A22
.=
{q}
by A1, FINSEQ_5:38
;
hence
x in {q}
by A15, A18, XBOOLE_0:def 4;
verum end; suppose that A23:
i + 1
= len (f -: q)
and A24:
j9 <> 0
;
x in {q}
1
<= j9
by A24, NAT_1:14;
then
(i + 1) + 1
<= j9 + (q .. f)
by A11, A23, XREAL_1:7;
then
i + 1
< j9 + (q .. f)
by NAT_1:13;
then
LSeg (
(f -: q),
i)
misses LSeg (
(f :- q),
j)
by A5, A16, A20;
then
(LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {}
;
hence
x in {q}
by A15, A18, XBOOLE_0:def 4;
verum end; suppose A25:
i + 1
<> len (f -: q)
;
x in {q}A26:
q .. f <= j9 + (q .. f)
by NAT_1:11;
i + 1
< q .. f
by A11, A14, A25, XXREAL_0:1;
then
i + 1
< j9 + (q .. f)
by A26, XXREAL_0:2;
then
LSeg (
(f -: q),
i)
misses LSeg (
(f :- q),
j)
by A5, A16, A20;
then
(LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {}
;
hence
x in {q}
by A15, A18, XBOOLE_0:def 4;
verum end; end;
end;
1 <= q .. f
by A1, FINSEQ_4:21;
then
1 < q .. f
by A2, XXREAL_0:1;
then
1 + 1 <= q .. f
by NAT_1:13;
then A27:
rng (f -: q) c= L~ (f -: q)
by A11, Th18;
(f -: q) /. (q .. f) = q
by A1, FINSEQ_5:45;
then
q in rng (f -: q)
by A11, A10, PARTFUN2:2;
then
q in (L~ (f -: q)) /\ (L~ (f :- q))
by A27, A9, A8, XBOOLE_0:def 4;
hence
{q} c= (L~ (f -: q)) /\ (L~ (f :- q))
by ZFMISC_1:31; verum