let f be FinSequence of (TOP-REAL 2); for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq holds
p in L~ (L_Cut (f,q))
let p, q be Point of (TOP-REAL 2); ( p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq implies p in L~ (L_Cut (f,q)) )
assume that
A1:
p in L~ f
and
A2:
q in L~ f
and
A3:
q <> f . (len f)
and
A4:
p = f . (len f)
and
A5:
f is being_S-Seq
; p in L~ (L_Cut (f,q))
1 + 1 <= len f
by A5, TOPREAL1:def 8;
then A6:
1 < len f
by XXREAL_0:2;
then A7:
(Index (p,f)) + 1 = len f
by A4, A5, JORDAN3:12;
AA:
len f in dom f
by A6, FINSEQ_3:25;
then AB: mid (f,(len f),(len f)) =
<*(f . (len f))*>
by FINSEQ_6:193
.=
<*(f /. (len f))*>
by AA, PARTFUN1:def 6
;
Index (q,f) < len f
by A2, JORDAN3:8;
then A8:
Index (q,f) <= Index (p,f)
by A7, NAT_1:13;
per cases
( Index (q,f) = Index (p,f) or Index (q,f) < Index (p,f) )
by A8, XXREAL_0:1;
suppose
Index (
q,
f)
= Index (
p,
f)
;
p in L~ (L_Cut (f,q))then A9:
L_Cut (
f,
q) =
<*q*> ^ (mid (f,(len f),(len f)))
by A3, A7, JORDAN3:def 3
.=
<*q*> ^ <*(f /. (len f))*>
by AB
.=
<*q,(f /. (len f))*>
by FINSEQ_1:def 9
.=
<*q,p*>
by A4, A6, FINSEQ_4:15
;
then
rng (L_Cut (f,q)) = {p,q}
by FINSEQ_2:127;
then A10:
p in rng (L_Cut (f,q))
by TARSKI:def 2;
len (L_Cut (f,q)) = 2
by A9, FINSEQ_1:44;
then
rng (L_Cut (f,q)) c= L~ (L_Cut (f,q))
by SPPOL_2:18;
hence
p in L~ (L_Cut (f,q))
by A10;
verum end;