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 A7: len (<*p*> ^ f) >= 2 by A5, XXREAL_0:2;
now :: thesis: not p in rng f
assume A8: 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, A8, 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 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: LSeg (f,i) misses LSeg (p,(f /. 1))
A15: 2 in dom f by A5, FINSEQ_3:25;
now :: thesis: not f /. 1 in LSeg (f,i)
assume f /. 1 in LSeg (f,i) ; :: thesis: contradiction
then 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 :: thesis: ( ( i = 1 + 1 & f /. 1 = f /. 2 ) or ( i > 1 + 1 & contradiction ) )
per cases ( i = 1 + 1 or i > 1 + 1 ) by A13, XXREAL_0:1;
case A18: i = 1 + 1 ; :: thesis: f /. 1 = f /. 2
then (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) = {(f /. 2)} by A14, TOPREAL1:def 6;
hence f /. 1 = f /. 2 by A16, A18, TARSKI:def 1; :: thesis: verum
end;
end;
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; :: thesis: 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)) ; :: thesis: 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 :: thesis: for i being Nat st 1 <= i & i + 2 <= len <*p*> holds
LSeg (<*p*>,i) misses LSeg (p,(f /. 1))
let i be 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)) )
A23: 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 A20, A23, 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, 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; :: thesis: verum