let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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)} ; :: thesis: <*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 10;
then A6: f /. 1 in LSeg f,1 by TOPREAL1:27;
set g = <*p*> ^ f;
A7: <*p*> is special by SPPOL_2:39;
len (<*p*> ^ f) = (len <*p*>) + (len f) by FINSEQ_1:35;
then len (<*p*> ^ f) >= len f by NAT_1:11;
then A8: len (<*p*> ^ f) >= 2 by A5, XXREAL_0:2;

now

assume A9: p in rng f ; :: thesis: contradiction
( rng f c= L~ f & p in LSeg p,(f /. 1) ) by A5, RLTOPSP1:69, SPPOL_2:18;
then p in {(f /. 1)} by A4, A9, XBOOLE_0:def 4;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

then {p} misses rng f by ZFMISC_1:56;
then ( <*p*> is one-to-one & rng <*p*> misses rng f ) by FINSEQ_1:56, FINSEQ_3:102;
then A10: <*p*> ^ f is one-to-one by FINSEQ_3:98;
L~ <*p*> = {} by SPPOL_2:12;
then (L~ <*p*>) /\ (L~ f) = {} ;
then A11: L~ <*p*> misses L~ f by XBOOLE_0:def 7;
A12: 1 in dom f by FINSEQ_5:6;

A13: now

let i be Element of NAT ; :: thesis: ( 1 + 1 <= i & i + 1 <= len f implies LSeg f,i misses LSeg p,(f /. 1) )
assume that
A14: 1 + 1 <= i and
A15: i + 1 <= len f ; :: thesis: LSeg f,i misses LSeg p,(f /. 1)
A16: 2 in dom f by A5, FINSEQ_3:27;

now

assume f /. 1 in LSeg f,i ; :: thesis: contradiction
then A17: f /. 1 in (LSeg f,1) /\ (LSeg f,i) by A6, XBOOLE_0:def 4;
then A18: LSeg f,1 meets LSeg f,i by XBOOLE_0:4;

now

per cases ( i = 1 + 1 or i > 1 + 1 ) by A14, XXREAL_0:1;

case A19: i = 1 + 1 ; :: thesis: f /. 1 = f /. 2

then (LSeg f,1) /\ (LSeg f,(1 + 1)) = {(f /. 2)} by A15, TOPREAL1:def 8;
hence f /. 1 = f /. 2 by A17, A19, TARSKI:def 1; :: thesis: verum

end;

case i > 1 + 1 ; :: thesis: contradiction

hence contradiction by A18, TOPREAL1:def 9; :: thesis: verum

end;

end;

end;

then f . 1 = f /. 2 by A12, PARTFUN1:def 8
.= f . 2 by A16, PARTFUN1:def 8 ;
hence contradiction by A12, A16, FUNCT_1:def 8; :: thesis: verum

end;

then not f /. 1 in (LSeg f,i) /\ (LSeg p,(f /. 1)) by XBOOLE_0:def 4;
then A20: (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:26, XBOOLE_1:26;
then (LSeg f,i) /\ (LSeg p,(f /. 1)) = {} by A20, ZFMISC_1:39;
hence LSeg f,i misses LSeg p,(f /. 1) by XBOOLE_0:def 7; :: thesis: verum

end;

A21: len <*p*> = 1 by FINSEQ_1:56;
then A22: ( <*p*> is s.n.c. & <*p*> /. (len <*p*>) = p ) by FINSEQ_4:25, SPPOL_2:34;

A23: now

let i be Element of NAT ; :: thesis: ( 1 <= i & i + 2 <= len <*p*> implies LSeg <*p*>,i misses LSeg p,(f /. 1) )
assume 1 <= i ; :: thesis: ( i + 2 <= len <*p*> implies LSeg <*p*>,i misses LSeg p,(f /. 1) )
A24: 2 <= i + 2 by NAT_1:11;
assume i + 2 <= len <*p*> ; :: thesis: LSeg <*p*>,i misses LSeg p,(f /. 1)
hence LSeg <*p*>,i misses LSeg p,(f /. 1) by A21, A24, XXREAL_0:2; :: thesis: verum

end;

(LSeg p,(f /. 1)) /\ (LSeg f,1) = {(f /. 1)} by A4, A6, TOPREAL3:26, ZFMISC_1:150;
then ( <*p*> ^ f is unfolded & <*p*> ^ f is s.n.c. & <*p*> ^ f is special ) by A3, A22, A11, A23, A13, A7, GOBOARD2:13, SPPOL_2:30, SPPOL_2:37;
hence <*p*> ^ f is S-Sequence_in_R2 by A10, A8, TOPREAL1:def 10; :: thesis: verum