let f be S-Sequence_in_R2; :: thesis: for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. 1 in Q holds

(L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

let Q be closed Subset of (TOP-REAL 2); :: thesis: ( L~ f meets Q & not f /. 1 in Q implies (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} )

assume that

A1: L~ f meets Q and

A2: not f /. 1 in Q ; :: thesis: (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

set p1 = f /. 1;

set p2 = f /. (len f);

set fp = First_Point ((L~ f),(f /. 1),(f /. (len f)),Q);

A3: (L~ f) /\ Q is closed by TOPS_1:8;

len f >= 1 + 1 by TOPREAL1:def 8;

then A4: len f > 1 by NAT_1:13;

then AA: 1 in dom f by FINSEQ_3:25;

L~ f is_an_arc_of f /. 1,f /. (len f) by TOPREAL1:25;

then A5: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A3, JORDAN5C:def 1;

then A6: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def 4;

then A7: 1 <= Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) by JORDAN3:8;

A8: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) <= len f by A6, JORDAN3:8;

then A9: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) in dom f by A7, FINSEQ_3:25;

1 in dom f by A4, FINSEQ_3:25;

then First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1 by A2, A28, PARTFUN1:def 6;

then First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A6, JORDAN5B:20;

then First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q by A28, XBOOLE_0:def 4;

hence (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by A10, ZFMISC_1:33; :: thesis: verum

(L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

let Q be closed Subset of (TOP-REAL 2); :: thesis: ( L~ f meets Q & not f /. 1 in Q implies (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} )

assume that

A1: L~ f meets Q and

A2: not f /. 1 in Q ; :: thesis: (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

set p1 = f /. 1;

set p2 = f /. (len f);

set fp = First_Point ((L~ f),(f /. 1),(f /. (len f)),Q);

A3: (L~ f) /\ Q is closed by TOPS_1:8;

len f >= 1 + 1 by TOPREAL1:def 8;

then A4: len f > 1 by NAT_1:13;

then AA: 1 in dom f by FINSEQ_3:25;

L~ f is_an_arc_of f /. 1,f /. (len f) by TOPREAL1:25;

then A5: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A3, JORDAN5C:def 1;

then A6: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def 4;

then A7: 1 <= Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) by JORDAN3:8;

A8: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) <= len f by A6, JORDAN3:8;

then A9: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) in dom f by A7, FINSEQ_3:25;

A10: now :: thesis: (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q c= {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}

A28:
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in Q
by A5, XBOOLE_0:def 4;assume
not (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q c= {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
; :: thesis: contradiction

then consider q being object such that

A11: q in (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q and

A12: not q in {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by TARSKI:def 3;

reconsider q = q as Point of (TOP-REAL 2) by A11;

A13: q in L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A11, XBOOLE_0:def 4;

A14: L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) c= L~ f by A6, JORDAN3:41;

A15: q <> First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) by A12, TARSKI:def 1;

q in Q by A11, XBOOLE_0:def 4;

then A16: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A3, A13, A14, JORDAN5C:15;

end;then consider q being object such that

A11: q in (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q and

A12: not q in {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by TARSKI:def 3;

reconsider q = q as Point of (TOP-REAL 2) by A11;

A13: q in L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A11, XBOOLE_0:def 4;

A14: L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) c= L~ f by A6, JORDAN3:41;

A15: q <> First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) by A12, TARSKI:def 1;

q in Q by A11, XBOOLE_0:def 4;

then A16: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A3, A13, A14, JORDAN5C:15;

per cases
( First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . 1 or First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1 )
;

end;

suppose A17:
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . 1
; :: thesis: contradiction

A18:
len <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> = 1
by FINSEQ_1:39;

q in L~ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> by A13, A17, JORDAN3:def 4;

hence contradiction by A18, TOPREAL1:22; :: thesis: verum

end;q in L~ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> by A13, A17, JORDAN3:def 4;

hence contradiction by A18, TOPREAL1:22; :: thesis: verum

suppose A19:
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1
; :: thesis: contradiction

set m = mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)));

A20: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) < len f by A6, JORDAN3:8;

len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) = ((Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) -' 1) + 1 by A7, A8, JORDAN4:8;

then A21: not mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) is empty by CARD_1:27;

A22: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) by A6, JORDAN3:9;

q in L~ ((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) ^ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*>) by A13, A19, JORDAN3:def 4;

then A23: q in (L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))) \/ (LSeg (((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A21, SPPOL_2:19;

end;A20: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) < len f by A6, JORDAN3:8;

len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) = ((Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) -' 1) + 1 by A7, A8, JORDAN4:8;

then A21: not mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) is empty by CARD_1:27;

A22: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) by A6, JORDAN3:9;

q in L~ ((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) ^ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*>) by A13, A19, JORDAN3:def 4;

then A23: q in (L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))) \/ (LSeg (((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A21, SPPOL_2:19;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( q in L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) or q in LSeg (((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))) )
by A23, XBOOLE_0:def 3;

end;

suppose A24:
q in L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))
; :: thesis: contradiction

f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) in LSeg ((f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))) by RLTOPSP1:68;

then LE f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)), First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A20, A22, A25, SPRECT_3:23;

then LE q, First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A26, JORDAN5C:13;

hence contradiction by A15, A16, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

end;

A25: now :: thesis: not Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) <= 1

then A26:
LE q,f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)), L~ f,f /. 1,f /. (len f)
by A8, A24, SPRECT_3:17;assume
Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) <= 1
; :: thesis: contradiction

then Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) = 1 by A7, XXREAL_0:1;

then len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) = 1 by AA, JORDAN4:15;

hence contradiction by A24, TOPREAL1:22; :: thesis: verum

end;then Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) = 1 by A7, XXREAL_0:1;

then len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) = 1 by AA, JORDAN4:15;

hence contradiction by A24, TOPREAL1:22; :: thesis: verum

f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) in LSeg ((f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))) by RLTOPSP1:68;

then LE f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)), First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A20, A22, A25, SPRECT_3:23;

then LE q, First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A26, JORDAN5C:13;

hence contradiction by A15, A16, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

suppose A27:
q in LSeg (((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))
; :: thesis: contradiction

len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) in dom (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))
by A21, FINSEQ_5:6;

then (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))) = (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) . (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))) by PARTFUN1:def 6

.= f . (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) by A7, A8, JORDAN4:10

.= f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) by A9, PARTFUN1:def 6 ;

then LE q, First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A7, A20, A22, A27, SPRECT_3:23;

hence contradiction by A15, A16, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

end;then (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))) = (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) . (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))) by PARTFUN1:def 6

.= f . (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) by A7, A8, JORDAN4:10

.= f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) by A9, PARTFUN1:def 6 ;

then LE q, First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A7, A20, A22, A27, SPRECT_3:23;

hence contradiction by A15, A16, JORDAN5C:12, TOPREAL1:25; :: thesis: verum

1 in dom f by A4, FINSEQ_3:25;

then First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1 by A2, A28, PARTFUN1:def 6;

then First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A6, JORDAN5B:20;

then First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q by A28, XBOOLE_0:def 4;

hence (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by A10, ZFMISC_1:33; :: thesis: verum