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: 1 in dom f by FINSEQ_5:6;
A6: len f >= 1 + 1 by TOPREAL1:def 10;
then A7: f /. 1 in LSeg f,1 by TOPREAL1:27;
set g = <*p*> ^ f;
<*p*> ^ f is being_S-Seq
proof
A8: <*p*> is one-to-one by FINSEQ_3:102;
now
assume A9: p in rng f ; :: thesis: contradiction
A10: rng f c= L~ f by A6, SPPOL_2:18;
p in LSeg p,(f /. 1) by TOPREAL1:6;
then p in {(f /. 1)} by A4, A9, A10, XBOOLE_0:def 4;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum
end;
then {p} misses rng f by ZFMISC_1:56;
then rng <*p*> misses rng f by FINSEQ_1:56;
hence <*p*> ^ f is one-to-one by A8, FINSEQ_3:98; :: according to TOPREAL1:def 10 :: thesis: ( 2 <= len (<*p*> ^ f) & <*p*> ^ f is unfolded & <*p*> ^ f is s.n.c. & <*p*> ^ f is special )
len (<*p*> ^ f) = (len <*p*>) + (len f) by FINSEQ_1:35;
then len (<*p*> ^ f) >= len f by NAT_1:11;
hence len (<*p*> ^ f) >= 2 by A6, XXREAL_0:2; :: thesis: ( <*p*> ^ f is unfolded & <*p*> ^ f is s.n.c. & <*p*> ^ f is special )
(LSeg p,(f /. 1)) /\ (LSeg f,1) = {(f /. 1)} by A4, A7, ZFMISC_1:150, TOPREAL3:26;
hence <*p*> ^ f is unfolded by SPPOL_2:30; :: thesis: ( <*p*> ^ f is s.n.c. & <*p*> ^ f is special )
A11: len <*p*> = 1 by FINSEQ_1:56;
then A12: <*p*> is s.n.c. by SPPOL_2:34;
A13: <*p*> /. (len <*p*>) = p by A11, FINSEQ_4:25;
L~ <*p*> = {} by SPPOL_2:12;
then (L~ <*p*>) /\ (L~ f) = {} ;
then A14: L~ <*p*> misses L~ f by XBOOLE_0:def 7;
A15: 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) )
assume A16: i + 2 <= len <*p*> ; :: thesis: LSeg <*p*>,i misses LSeg p,(f /. 1)
2 <= i + 2 by NAT_1:11;
hence LSeg <*p*>,i misses LSeg p,(f /. 1) by A11, A16, XXREAL_0:2; :: thesis: verum
end;
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
A17: 1 + 1 <= i and
A18: i + 1 <= len f ; :: thesis: LSeg f,i misses LSeg p,(f /. 1)
A19: 2 in dom f by A6, FINSEQ_3:27;
now
assume f /. 1 in LSeg f,i ; :: thesis: contradiction
then A20: f /. 1 in (LSeg f,1) /\ (LSeg f,i) by A7, XBOOLE_0:def 4;
then A21: LSeg f,1 meets LSeg f,i by XBOOLE_0:4;
now
per cases ( i = 1 + 1 or i > 1 + 1 ) by A17, XXREAL_0:1;
case A22: i = 1 + 1 ; :: thesis: f /. 1 = f /. 2
then (LSeg f,1) /\ (LSeg f,(1 + 1)) = {(f /. 2)} by A18, TOPREAL1:def 8;
hence f /. 1 = f /. 2 by A20, A22, TARSKI:def 1; :: thesis: verum
end;
end;
end;
then f . 1 = f /. 2 by A5, PARTFUN1:def 8
.= f . 2 by A19, PARTFUN1:def 8 ;
hence contradiction by A5, A19, 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 A23: (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 A23, ZFMISC_1:39;
hence LSeg f,i misses LSeg p,(f /. 1) by XBOOLE_0:def 7; :: thesis: verum
end;
hence <*p*> ^ f is s.n.c. by A12, A13, A14, A15, SPPOL_2:37; :: thesis: <*p*> ^ f is special
A24: <*p*> is special by SPPOL_2:39;
<*p*> /. (len <*p*>) = <*p*> /. 1 by FINSEQ_1:56
.= p by FINSEQ_4:25 ;
hence <*p*> ^ f is special by A3, A24, GOBOARD2:13; :: thesis: verum
end;
hence <*p*> ^ f is S-Sequence_in_R2 ; :: thesis: verum