let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st f is being_S-Seq & p <> f /. 1 & ( p `1 = (f /. 1) `1 or p `2 = (f /. 1) `2 ) & (LSeg (p,(f /. 1))) /\ (L~ f) = {(f /. 1)} holds
<*p*> ^ f is S-Sequence_in_R2
let p be Point of (TOP-REAL 2); ( f is being_S-Seq & p <> f /. 1 & ( p `1 = (f /. 1) `1 or p `2 = (f /. 1) `2 ) & (LSeg (p,(f /. 1))) /\ (L~ f) = {(f /. 1)} implies <*p*> ^ f is S-Sequence_in_R2 )
assume that
A1:
f is being_S-Seq
and
A2:
p <> f /. 1
and
A3:
( p `1 = (f /. 1) `1 or p `2 = (f /. 1) `2 )
and
A4:
(LSeg (p,(f /. 1))) /\ (L~ f) = {(f /. 1)}
; <*p*> ^ f is S-Sequence_in_R2
reconsider f = f as S-Sequence_in_R2 by A1;
A5:
len f >= 1 + 1
by TOPREAL1:def 8;
then A6:
f /. 1 in LSeg (f,1)
by TOPREAL1:21;
set g = <*p*> ^ f;
len (<*p*> ^ f) = (len <*p*>) + (len f)
by FINSEQ_1:22;
then
len (<*p*> ^ f) >= len f
by NAT_1:11;
then A7:
len (<*p*> ^ f) >= 2
by A5, XXREAL_0:2;
then
{p} misses rng f
by ZFMISC_1:50;
then
( <*p*> is one-to-one & rng <*p*> misses rng f )
by FINSEQ_1:39, FINSEQ_3:93;
then A9:
<*p*> ^ f is one-to-one
by FINSEQ_3:91;
L~ <*p*> = {}
by SPPOL_2:12;
then
(L~ <*p*>) /\ (L~ f) = {}
;
then A10:
L~ <*p*> misses L~ f
;
A11:
1 in dom f
by FINSEQ_5:6;
A12:
now for i being Nat st 1 + 1 <= i & i + 1 <= len f holds
LSeg (f,i) misses LSeg (p,(f /. 1))let i be
Nat;
( 1 + 1 <= i & i + 1 <= len f implies LSeg (f,i) misses LSeg (p,(f /. 1)) )assume that A13:
1
+ 1
<= i
and A14:
i + 1
<= len f
;
LSeg (f,i) misses LSeg (p,(f /. 1))A15:
2
in dom f
by A5, FINSEQ_3:25;
now not f /. 1 in LSeg (f,i)assume
f /. 1
in LSeg (
f,
i)
;
contradictionthen A16:
f /. 1
in (LSeg (f,1)) /\ (LSeg (f,i))
by A6, XBOOLE_0:def 4;
then A17:
LSeg (
f,1)
meets LSeg (
f,
i)
;
now ( ( i = 1 + 1 & f /. 1 = f /. 2 ) or ( i > 1 + 1 & contradiction ) )end; then f . 1 =
f /. 2
by A11, PARTFUN1:def 6
.=
f . 2
by A15, PARTFUN1:def 6
;
hence
contradiction
by A11, A15, FUNCT_1:def 4;
verum end; then
not
f /. 1
in (LSeg (f,i)) /\ (LSeg (p,(f /. 1)))
by XBOOLE_0:def 4;
then A19:
(LSeg (f,i)) /\ (LSeg (p,(f /. 1))) <> {(f /. 1)}
by TARSKI:def 1;
(LSeg (f,i)) /\ (LSeg (p,(f /. 1))) c= {(f /. 1)}
by A4, TOPREAL3:19, XBOOLE_1:26;
then
(LSeg (f,i)) /\ (LSeg (p,(f /. 1))) = {}
by A19, ZFMISC_1:33;
hence
LSeg (
f,
i)
misses LSeg (
p,
(f /. 1))
;
verum end;
A20:
len <*p*> = 1
by FINSEQ_1:39;
then A21:
( <*p*> is s.n.c. & <*p*> /. (len <*p*>) = p )
by FINSEQ_4:16, SPPOL_2:33;
A22:
now for i being Nat st 1 <= i & i + 2 <= len <*p*> holds
LSeg (<*p*>,i) misses LSeg (p,(f /. 1))let i be
Nat;
( 1 <= i & i + 2 <= len <*p*> implies LSeg (<*p*>,i) misses LSeg (p,(f /. 1)) )assume
1
<= i
;
( i + 2 <= len <*p*> implies LSeg (<*p*>,i) misses LSeg (p,(f /. 1)) )A23:
2
<= i + 2
by NAT_1:11;
assume
i + 2
<= len <*p*>
;
LSeg (<*p*>,i) misses LSeg (p,(f /. 1))hence
LSeg (
<*p*>,
i)
misses LSeg (
p,
(f /. 1))
by A20, A23, XXREAL_0:2;
verum end;
(LSeg (p,(f /. 1))) /\ (LSeg (f,1)) = {(f /. 1)}
by A4, A6, TOPREAL3:19, ZFMISC_1:124;
then
( <*p*> ^ f is unfolded & <*p*> ^ f is s.n.c. & <*p*> ^ f is special )
by A3, A21, A10, A22, A12, GOBOARD2:8, SPPOL_2:29, SPPOL_2:36;
hence
<*p*> ^ f is S-Sequence_in_R2
by A9, A7, TOPREAL1:def 8; verum