let p be Point of (TOP-REAL 2); :: thesis: for f, h being FinSequence of (TOP-REAL 2)
for r being Real
for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[(p `1),((f /. (len f)) `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[(p `1),((f /. (len f)) `2)]|,p*> & ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )
let f, h be FinSequence of (TOP-REAL 2); :: thesis: for r being Real
for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[(p `1),((f /. (len f)) `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[(p `1),((f /. (len f)) `2)]|,p*> & ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )
let r be Real; :: thesis: for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[(p `1),((f /. (len f)) `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[(p `1),((f /. (len f)) `2)]|,p*> & ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )
let u be Point of (Euclid 2); :: thesis: ( f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[(p `1),((f /. (len f)) `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[(p `1),((f /. (len f)) `2)]|,p*> & ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p))) /\ (L~ f) = {(f /. (len f))} implies ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) )
set p1 = f /. 1;
set p2 = f /. (len f);
assume that
A1: f /. (len f) in Ball (u,r) and
A2: p in Ball (u,r) and
A3: |[(p `1),((f /. (len f)) `2)]| in Ball (u,r) and
A4: f is being_S-Seq and
A5: p `1 <> (f /. (len f)) `1 and
A6: p `2 <> (f /. (len f)) `2 and
A7: h = f ^ <*|[(p `1),((f /. (len f)) `2)]|,p*> and
A8: ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p))) /\ (L~ f) = {(f /. (len f))} ; :: thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )
set p3 = |[(p `1),((f /. (len f)) `2)]|;
set f1 = f ^ <*|[(p `1),((f /. (len f)) `2)]|*>;
set h1 = (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ^ <*p*>;
reconsider Lf = L~ f as non empty Subset of (TOP-REAL 2) by A8;
A9: f /. (len f) in LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|) by RLTOPSP1:68;
L~ f is_S-P_arc_joining f /. 1,f /. (len f) by A4;
then Lf is_an_arc_of f /. 1,f /. (len f) by Th2;
then f /. (len f) in L~ f by TOPREAL1:1;
then f /. (len f) in (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f) by A9, XBOOLE_0:def 4;
then A10: ( (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f) c= ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f)) \/ ((LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ f)) & {(f /. (len f))} c= (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f) ) by XBOOLE_1:7, ZFMISC_1:31;
{(f /. (len f))} = ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f)) \/ ((LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ f)) by A8, XBOOLE_1:23;
then A11: (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f) = {(f /. (len f))} by A10;
A12: len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) = (len f) + (len <*|[(p `1),((f /. (len f)) `2)]|*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
then A13: (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) /. (len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) = |[(p `1),((f /. (len f)) `2)]| by FINSEQ_4:67;
A14: p = |[(p `1),(p `2)]| by EUCLID:53;
A15: Seg (len f) = dom f by FINSEQ_1:def 3;
len f >= 2 by A4;
then A16: 1 <= len f by XXREAL_0:2;
then len f in dom f by A15, FINSEQ_1:1;
then A17: (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) /. (len f) = f /. (len f) by FINSEQ_4:68;
A18: (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) c= {|[(p `1),((f /. (len f)) `2)]|}
proof
set M1 = { (LSeg ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ) } ;
set Mf = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;
assume not (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) c= {|[(p `1),((f /. (len f)) `2)]|} ; :: thesis: contradiction
then consider x being object such that
A19: x in (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) and
A20: not x in {|[(p `1),((f /. (len f)) `2)]|} ;
x in L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) by A19, XBOOLE_0:def 4;
then consider X being set such that
A21: x in X and
A22: X in { (LSeg ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ) } by TARSKI:def 4;
consider k being Nat such that
A23: X = LSeg ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>),k) and
A24: 1 <= k and
A25: k + 1 <= len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) by A22;
A26: x in LSeg (|[(p `1),((f /. (len f)) `2)]|,p) by A19, XBOOLE_0:def 4;
now :: thesis: contradiction
per cases ( k + 1 = len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) or k + 1 < len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ) by A25, XXREAL_0:1;
suppose k + 1 = len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ; :: thesis: contradiction
then LSeg ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>),k) = LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|) by A12, A13, A17, A24, TOPREAL1:def 3;
then x in (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) by A26, A21, A23, XBOOLE_0:def 4;
hence contradiction by A20, TOPREAL3:30; :: thesis: verum
end;
suppose k + 1 < len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ; :: thesis: contradiction
then A27: k + 1 <= len f by A12, NAT_1:13;
k <= k + 1 by NAT_1:11;
then k <= len f by A27, XXREAL_0:2;
then A28: k in dom f by A15, A24, FINSEQ_1:1;
1 <= k + 1 by A24, NAT_1:13;
then k + 1 in dom f by A15, A27, FINSEQ_1:1;
then X = LSeg (f,k) by A23, A28, TOPREAL3:18;
then X in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A24, A27;
then A29: x in L~ f by A21, TARSKI:def 4;
x in (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) by A26, XBOOLE_0:def 3;
then x in {(f /. (len f))} by A8, A29, XBOOLE_0:def 4;
then x = f /. (len f) by TARSKI:def 1;
hence contradiction by A5, A14, A26, TOPREAL3:11; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
A30: (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ^ <*p*> = f ^ (<*|[(p `1),((f /. (len f)) `2)]|*> ^ <*p*>) by FINSEQ_1:32
.= h by A7, FINSEQ_1:def 9 ;
A31: ( |[(p `1),((f /. (len f)) `2)]| `2 = (f /. (len f)) `2 & |[(p `1),((f /. (len f)) `2)]| `1 = p `1 ) by EUCLID:52;
then A32: f ^ <*|[(p `1),((f /. (len f)) `2)]|*> is being_S-Seq by A1, A3, A4, A5, A11, Th19;
A33: L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) is_S-P_arc_joining f /. 1,|[(p `1),((f /. (len f)) `2)]| by A1, A3, A4, A5, A31, A11, Th19;
then reconsider Lf1 = L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) as non empty Subset of (TOP-REAL 2) by Th1, TOPREAL1:26;
A34: |[(p `1),((f /. (len f)) `2)]| in LSeg (|[(p `1),((f /. (len f)) `2)]|,p) by RLTOPSP1:68;
A35: (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) /. (len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) = |[(p `1),((f /. (len f)) `2)]| by A12, FINSEQ_4:67;
L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) c= (L~ f) \/ (Ball (u,r)) by A1, A3, A4, A5, A31, A11, Th19;
then (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) \/ (Ball (u,r)) c= ((L~ f) \/ (Ball (u,r))) \/ (Ball (u,r)) by XBOOLE_1:9;
then A36: (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) \/ (Ball (u,r)) c= (L~ f) \/ ((Ball (u,r)) \/ (Ball (u,r))) by XBOOLE_1:4;
A37: ( ( p `1 = |[(p `1),((f /. (len f)) `2)]| `1 & p `2 <> |[(p `1),((f /. (len f)) `2)]| `2 ) or ( p `1 <> |[(p `1),((f /. (len f)) `2)]| `1 & p `2 = |[(p `1),((f /. (len f)) `2)]| `2 ) ) by A6, EUCLID:52;
Lf1 is_an_arc_of f /. 1,|[(p `1),((f /. (len f)) `2)]| by A33, Th2;
then |[(p `1),((f /. (len f)) `2)]| in L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) by TOPREAL1:1;
then |[(p `1),((f /. (len f)) `2)]| in (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) by A34, XBOOLE_0:def 4;
then {|[(p `1),((f /. (len f)) `2)]|} c= (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) by ZFMISC_1:31;
then A38: (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) = {|[(p `1),((f /. (len f)) `2)]|} by A18;
1 in dom f by A15, A16, FINSEQ_1:1;
then (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) /. 1 = f /. 1 by FINSEQ_4:68;
hence L~ h is_S-P_arc_joining f /. 1,p by A2, A3, A37, A32, A35, A38, A30, Th19; :: thesis: L~ h c= (L~ f) \/ (Ball (u,r))
L~ ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ^ <*p*>) c= (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) \/ (Ball (u,r)) by A2, A3, A37, A32, A35, A38, Th19;
hence L~ h c= (L~ f) \/ (Ball (u,r)) by A30, A36; :: thesis: verum