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 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 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:68, 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:50;
then ( <*p*> is one-to-one & rng <*p*> misses rng f ) by FINSEQ_1:39, FINSEQ_3:93;
then A10: <*p*> ^ f is one-to-one by FINSEQ_3:91;
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:25;

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 6;
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 7; :: thesis: verum

end;

end;

end;

then f . 1 = f /. 2 by A12, PARTFUN1:def 6
.= f . 2 by A16, PARTFUN1:def 6 ;
hence contradiction by A12, A16, FUNCT_1:def 4; :: 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:19, XBOOLE_1:26;
then (LSeg (f,i)) /\ (LSeg (p,(f /. 1))) = {} by A20, ZFMISC_1:33;
hence LSeg (f,i) misses LSeg (p,(f /. 1)) by XBOOLE_0:def 7; :: thesis: verum

end;

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

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:19, ZFMISC_1:124;
then ( <*p*> ^ f is unfolded & <*p*> ^ f is s.n.c. & <*p*> ^ f is special ) by A3, A22, A11, A23, A13, GOBOARD2:8, SPPOL_2:29, SPPOL_2:36;
hence <*p*> ^ f is S-Sequence_in_R2 by A10, A8, TOPREAL1:def 8; :: thesis: verum