let p be Point of (TOP-REAL 2); :: thesis: for f, h being FinSequence of (TOP-REAL 2)
for i being Element of NAT st f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg (f,i) & p <> f /. i & h = (f | i) ^ <*p*> holds
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
let f, h be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of NAT st f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg (f,i) & p <> f /. i & h = (f | i) ^ <*p*> holds
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
let i be Element of NAT ; :: thesis: ( f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg (f,i) & p <> f /. i & h = (f | i) ^ <*p*> implies ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) )
set p1 = f /. 1;
set q = f /. i;
assume that
A1: f is being_S-Seq and
A2: i in dom f and
A3: i + 1 in dom f and
A4: i > 1 and
A5: p in LSeg (f,i) and
A6: p <> f /. i and
A7: h = (f | i) ^ <*p*> ; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
A8: f is one-to-one by A1, TOPREAL1:def 8;
set v = f | i;
A9: f | i = f | (Seg i) by FINSEQ_1:def 15;
then A10: dom (f | i) = (dom f) /\ (Seg i) by RELAT_1:61;
A11: Seg (len h) = dom h by FINSEQ_1:def 3;
A12: f is unfolded by A1, TOPREAL1:def 8;
A13: f is special by A1, TOPREAL1:def 8;
A14: f is s.n.c. by A1, TOPREAL1:def 8;
set q1 = f /. i;
set q2 = f /. (i + 1);
A15: Seg (len f) = dom f by FINSEQ_1:def 3;
then A16: i + 1 <= len f by A3, FINSEQ_1:1;
then A17: p in LSeg ((f /. i),(f /. (i + 1))) by A4, A5, TOPREAL1:def 3;
A18: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, A16, TOPREAL1:def 3;
A19: LSeg (f,i) = LSeg ((f /. (i + 1)),(f /. i)) by A4, A16, TOPREAL1:def 3;
i <> i + 1 ;
then A20: f /. i <> f /. (i + 1) by A2, A3, A8, PARTFUN2:10;
A21: f /. i in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;
A22: ( f /. i = |[((f /. i) `1),((f /. i) `2)]| & f /. (i + 1) = |[((f /. (i + 1)) `1),((f /. (i + 1)) `2)]| ) by EUCLID:53;
A23: i <= len f by A2, A15, FINSEQ_1:1;
then Seg i c= dom f by A15, FINSEQ_1:5;
then A24: dom (f | i) = Seg i by A10, XBOOLE_1:28;
then A25: len (f | i) = i by FINSEQ_1:def 3;
then A26: len h = i + (len <*p*>) by A7, FINSEQ_1:22
.= i + 1 by FINSEQ_1:39 ;
then A27: h /. (len h) = p by A7, A25, FINSEQ_4:67;
A28: i in dom (f | i) by A4, A24, FINSEQ_1:1;
then A29: h /. i = (f | i) /. i by A7, FINSEQ_4:68
.= f /. i by A28, FINSEQ_4:70 ;
then A30: LSeg (h,i) = LSeg ((f /. i),p) by A4, A26, A27, TOPREAL1:def 3;
A31: 1 + 1 <= i by A4, NAT_1:13;
thus A32: h is being_S-Seq :: thesis: ( h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
proof
now
set Z = { m where m is Element of NAT : ( 1 <= m & m <= len h ) } ;
given x, y being set such that A33: x in dom h and
A34: y in dom h and
A35: h . x = h . y and
A36: x <> y ; :: thesis: contradiction
x in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A11, A33, FINSEQ_1:def 1;
then consider k1 being Element of NAT such that
A37: k1 = x and
A38: 1 <= k1 and
A39: k1 <= len h ;
y in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A11, A34, FINSEQ_1:def 1;
then consider k2 being Element of NAT such that
A40: k2 = y and
A41: 1 <= k2 and
A42: k2 <= len h ;
A43: h /. k1 = h . y by A33, A35, A37, PARTFUN1:def 6
.= h /. k2 by A34, A40, PARTFUN1:def 6 ;
k2 <= len f by A26, A16, A42, XXREAL_0:2;
then A44: k2 in dom f by A15, A41, FINSEQ_1:1;
k1 <= len f by A26, A16, A39, XXREAL_0:2;
then A45: k1 in dom f by A15, A38, FINSEQ_1:1;
A46: k1 + (1 + 1) = (k1 + 1) + 1 ;
A47: k2 + (1 + 1) = (k2 + 1) + 1 ;
now
per cases ( ( k1 = i + 1 & k2 = i + 1 ) or ( k1 = i + 1 & k2 < i + 1 ) or ( k1 < i + 1 & k2 = i + 1 ) or ( k1 < i + 1 & k2 < i + 1 ) ) by A26, A39, A42, XXREAL_0:1;
suppose ( k1 = i + 1 & k2 = i + 1 ) ; :: thesis: contradiction
hence contradiction by A36, A37, A40; :: thesis: verum
end;
suppose A48: ( k1 = i + 1 & k2 < i + 1 ) ; :: thesis: contradiction
then A49: k2 + 1 <= k1 by NAT_1:13;
now
per cases ( k2 + 1 = k1 or k2 + 1 < k1 ) by A49, XXREAL_0:1;
suppose k2 + 1 < k1 ; :: thesis: contradiction
then A50: k2 + 1 <= i by A48, NAT_1:13;
now
per cases ( k2 + 1 = i or k2 + 1 < i ) by A50, XXREAL_0:1;
suppose A51: k2 + 1 = i ; :: thesis: contradiction
then k2 <= i by NAT_1:11;
then A52: k2 in dom (f | i) by A24, A41, FINSEQ_1:1;
then A53: h /. k2 = (f | i) /. k2 by A7, FINSEQ_4:68
.= f /. k2 by A52, FINSEQ_4:70 ;
k2 + 1 <= len f by A2, A15, A51, FINSEQ_1:1;
then A54: f /. k2 in LSeg (f,k2) by A41, TOPREAL1:21;
(LSeg (f,k2)) /\ (LSeg (f,i)) = {(f /. i)} by A12, A16, A41, A47, A51, TOPREAL1:def 6;
then f /. k2 in {(f /. i)} by A5, A26, A27, A43, A48, A54, A53, XBOOLE_0:def 4;
then A55: f /. k2 = f /. i by TARSKI:def 1;
k2 < i by A51, NAT_1:13;
hence contradiction by A2, A8, A44, A55, PARTFUN2:10; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A60: ( k1 < i + 1 & k2 = i + 1 ) ; :: thesis: contradiction
then A61: k1 + 1 <= k2 by NAT_1:13;
now
per cases ( k1 + 1 = k2 or k1 + 1 < k2 ) by A61, XXREAL_0:1;
suppose k1 + 1 < k2 ; :: thesis: contradiction
then A62: k1 + 1 <= i by A60, NAT_1:13;
now
per cases ( k1 + 1 = i or k1 + 1 < i ) by A62, XXREAL_0:1;
suppose A63: k1 + 1 = i ; :: thesis: contradiction
then k1 <= i by NAT_1:11;
then A64: k1 in dom (f | i) by A24, A38, FINSEQ_1:1;
then A65: h /. k1 = (f | i) /. k1 by A7, FINSEQ_4:68
.= f /. k1 by A64, FINSEQ_4:70 ;
k1 + 1 <= len f by A2, A15, A63, FINSEQ_1:1;
then A66: f /. k1 in LSeg (f,k1) by A38, TOPREAL1:21;
(LSeg (f,k1)) /\ (LSeg (f,i)) = {(f /. i)} by A12, A16, A38, A46, A63, TOPREAL1:def 6;
then f /. k1 in {(f /. i)} by A5, A26, A27, A43, A60, A66, A65, XBOOLE_0:def 4;
then A67: f /. k1 = f /. i by TARSKI:def 1;
k1 < i by A63, NAT_1:13;
hence contradiction by A2, A8, A45, A67, PARTFUN2:10; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A72: ( k1 < i + 1 & k2 < i + 1 ) ; :: thesis: contradiction
then k2 <= i by NAT_1:13;
then A73: k2 in dom (f | i) by A24, A41, FINSEQ_1:1;
k1 <= i by A72, NAT_1:13;
then A74: k1 in dom (f | i) by A24, A38, FINSEQ_1:1;
then f . k1 = (f | i) . k1 by A9, FUNCT_1:47
.= h . k1 by A7, A74, FINSEQ_1:def 7
.= (f | i) . k2 by A7, A35, A37, A40, A73, FINSEQ_1:def 7
.= f . k2 by A9, A73, FUNCT_1:47 ;
hence contradiction by A8, A36, A37, A40, A45, A44, FUNCT_1:def 4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence h is one-to-one by FUNCT_1:def 4; :: according to TOPREAL1:def 8 :: thesis: ( 2 <= len h & h is unfolded & h is s.n.c. & h is special )
thus len h >= 2 by A4, A26, A31, XREAL_1:6; :: thesis: ( h is unfolded & h is s.n.c. & h is special )
thus h is unfolded :: thesis: ( h is s.n.c. & h is special )
proof
let j be Nat; :: according to TOPREAL1:def 6 :: thesis: ( not 1 <= j or not j + 2 <= len h or (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} )
assume that
A75: 1 <= j and
A76: j + 2 <= len h ; :: thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}
A77: 1 <= j + 1 by NAT_1:11;
(j + 1) + 1 = j + (1 + 1) ;
then j + 1 <= i by A26, A76, XREAL_1:6;
then A78: j + 1 in dom (f | i) by A24, A77, FINSEQ_1:1;
then A79: h /. (j + 1) = (f | i) /. (j + 1) by A7, FINSEQ_4:68
.= f /. (j + 1) by A78, FINSEQ_4:70 ;
(i + 1) + 1 = i + (1 + 1) ;
then len h <= i + 2 by A26, NAT_1:11;
then j + 2 <= i + 2 by A76, XXREAL_0:2;
then j <= i by XREAL_1:6;
then A80: j in dom (f | i) by A24, A75, FINSEQ_1:1;
then A81: LSeg (h,j) = LSeg ((f | i),j) by A7, A78, TOPREAL3:18
.= LSeg (f,j) by A80, A78, TOPREAL3:17 ;
j <= j + 2 by NAT_1:11;
then A82: 1 <= j + (1 + 1) by A75, XXREAL_0:2;
A83: j + (1 + 1) = (j + 1) + 1 ;
i + 1 in Seg (len f) by A3, FINSEQ_1:def 3;
then len h <= len f by A26, FINSEQ_1:1;
then A84: j + 2 <= len f by A76, XXREAL_0:2;
then A85: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A12, A75, TOPREAL1:def 6;
now
per cases ( j + 2 = len h or j + 2 < len h ) by A76, XXREAL_0:1;
suppose A86: j + 2 = len h ; :: thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}
j + 1 <= (j + 1) + 1 by NAT_1:11;
then j + 1 <= len h by A76, XXREAL_0:2;
then A87: h /. (j + 1) in LSeg (h,j) by A75, TOPREAL1:21;
h /. (j + 1) in LSeg (h,(j + 1)) by A76, A77, A83, TOPREAL1:21;
then h /. (j + 1) in (LSeg (h,j)) /\ (LSeg (h,(j + 1))) by A87, XBOOLE_0:def 4;
then A88: {(h /. (j + 1))} c= (LSeg (h,j)) /\ (LSeg (h,(j + 1))) by ZFMISC_1:31;
(LSeg (h,j)) /\ (LSeg (h,(j + 1))) c= {(h /. (j + 1))} by A26, A18, A21, A17, A30, A85, A81, A79, A86, TOPREAL1:6, XBOOLE_1:26;
hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} by A88, XBOOLE_0:def 10; :: thesis: verum
end;
suppose j + 2 < len h ; :: thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}
then j + (1 + 1) <= i by A26, NAT_1:13;
then A89: (j + 1) + 1 in dom (f | i) by A24, A82, FINSEQ_1:1;
then LSeg (h,(j + 1)) = LSeg ((f | i),(j + 1)) by A7, A78, TOPREAL3:18
.= LSeg (f,(j + 1)) by A78, A89, TOPREAL3:17 ;
hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} by A12, A75, A84, A81, A79, TOPREAL1:def 6; :: thesis: verum
end;
end;
end;
hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} ; :: thesis: verum
end;
thus h is s.n.c. :: thesis: h is special
proof
let n, m be Nat; :: according to TOPREAL1:def 7 :: thesis: ( m <= n + 1 or LSeg (h,n) misses LSeg (h,m) )
assume A90: m > n + 1 ; :: thesis: LSeg (h,n) misses LSeg (h,m)
n <= n + 1 by NAT_1:11;
then A91: n <= m by A90, XXREAL_0:2;
A92: 1 <= n + 1 by NAT_1:11;
A93: LSeg (f,n) misses LSeg (f,m) by A14, A90, TOPREAL1:def 7;
now
per cases ( m + 1 < len h or m + 1 = len h or m + 1 > len h ) by XXREAL_0:1;
suppose A94: m + 1 < len h ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
A95: 1 < m by A90, A92, XXREAL_0:2;
then A96: 1 <= m + 1 by NAT_1:13;
m + 1 <= i by A26, A94, NAT_1:13;
then A97: m + 1 in dom (f | i) by A24, A96, FINSEQ_1:1;
A98: m <= i by A26, A94, XREAL_1:6;
then A99: m in dom (f | i) by A24, A95, FINSEQ_1:1;
then A100: LSeg (h,m) = LSeg ((f | i),m) by A7, A97, TOPREAL3:18
.= LSeg (f,m) by A99, A97, TOPREAL3:17 ;
now
per cases ( 0 < n or 0 = n ) ;
suppose 0 < n ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
then A101: 0 + 1 <= n by NAT_1:13;
n + 1 <= i by A90, A98, XXREAL_0:2;
then A102: n + 1 in dom (f | i) by A24, A92, FINSEQ_1:1;
n <= i by A91, A98, XXREAL_0:2;
then A103: n in dom (f | i) by A24, A101, FINSEQ_1:1;
then LSeg (h,n) = LSeg ((f | i),n) by A7, A102, TOPREAL3:18
.= LSeg (f,n) by A103, A102, TOPREAL3:17 ;
then LSeg (h,n) misses LSeg (h,m) by A14, A90, A100, TOPREAL1:def 7;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} by XBOOLE_0:def 7; :: thesis: verum
end;
suppose 0 = n ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
then LSeg (h,n) = {} by TOPREAL1:def 3;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
suppose A104: m + 1 = len h ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
A105: (LSeg (f,n)) /\ (LSeg (f,m)) = {} by A93, XBOOLE_0:def 7;
now
per cases ( 0 < n or 0 = n ) ;
suppose 0 < n ; :: thesis: {} = (LSeg (h,n)) /\ (LSeg (h,m))
then 0 + 1 <= n by NAT_1:13;
then A106: n in dom (f | i) by A24, A26, A91, A104, FINSEQ_1:1;
A107: n + 1 in dom (f | i) by A24, A26, A90, A92, A104, FINSEQ_1:1;
then LSeg (h,n) = LSeg ((f | i),n) by A7, A106, TOPREAL3:18
.= LSeg (f,n) by A106, A107, TOPREAL3:17 ;
hence {} = (LSeg (h,m)) /\ ((LSeg (f,m)) /\ (LSeg (h,n))) by A105
.= ((LSeg (h,m)) /\ (LSeg (f,m))) /\ (LSeg (h,n)) by XBOOLE_1:16
.= (LSeg (h,n)) /\ (LSeg (h,m)) by A26, A18, A21, A17, A30, A104, TOPREAL1:6, XBOOLE_1:28 ;
:: thesis: verum
end;
suppose 0 = n ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
then LSeg (h,n) = {} by TOPREAL1:def 3;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
suppose m + 1 > len h ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
then LSeg (h,m) = {} by TOPREAL1:def 3;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum
end;
let n be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= n or not n + 1 <= len h or (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
assume that
A108: 1 <= n and
A109: n + 1 <= len h ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
set p3 = h /. n;
set p4 = h /. (n + 1);
now
per cases ( n + 1 = len h or n + 1 < len h ) by A109, XXREAL_0:1;
suppose A110: n + 1 = len h ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
A111: i in dom (f | i) by A4, A24, FINSEQ_1:1;
then A112: h /. n = (f | i) /. i by A7, A26, A110, FINSEQ_4:68
.= f /. i by A111, FINSEQ_4:70 ;
now
per cases ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A4, A13, A16, TOPREAL1:def 5;
suppose A113: (f /. i) `1 = (f /. (i + 1)) `1 ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
then A114: (f /. i) `2 <> (f /. (i + 1)) `2 by A20, TOPREAL3:6;
now
per cases ( (f /. i) `2 < (f /. (i + 1)) `2 or (f /. (i + 1)) `2 < (f /. i) `2 ) by A114, XXREAL_0:1;
suppose (f /. i) `2 < (f /. (i + 1)) `2 ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
then p in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `1 = (f /. i) `1 & (f /. i) `2 <= p11 `2 & p11 `2 <= (f /. (i + 1)) `2 ) } by A5, A19, A22, A113, TOPREAL3:9;
then ex p11 being Point of (TOP-REAL 2) st
( p = p11 & p11 `1 = (f /. i) `1 & (f /. i) `2 <= p11 `2 & p11 `2 <= (f /. (i + 1)) `2 ) ;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A7, A25, A26, A110, A112, FINSEQ_4:67; :: thesis: verum
end;
suppose (f /. (i + 1)) `2 < (f /. i) `2 ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
then p in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `1 = (f /. i) `1 & (f /. (i + 1)) `2 <= p22 `2 & p22 `2 <= (f /. i) `2 ) } by A5, A19, A22, A113, TOPREAL3:9;
then ex p11 being Point of (TOP-REAL 2) st
( p = p11 & p11 `1 = (f /. i) `1 & (f /. (i + 1)) `2 <= p11 `2 & p11 `2 <= (f /. i) `2 ) ;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A7, A25, A26, A110, A112, FINSEQ_4:67; :: thesis: verum
end;
end;
end;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; :: thesis: verum
end;
suppose A115: (f /. i) `2 = (f /. (i + 1)) `2 ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
then A116: (f /. i) `1 <> (f /. (i + 1)) `1 by A20, TOPREAL3:6;
now
per cases ( (f /. i) `1 < (f /. (i + 1)) `1 or (f /. (i + 1)) `1 < (f /. i) `1 ) by A116, XXREAL_0:1;
suppose (f /. i) `1 < (f /. (i + 1)) `1 ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
then p in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `2 = (f /. i) `2 & (f /. i) `1 <= p11 `1 & p11 `1 <= (f /. (i + 1)) `1 ) } by A5, A19, A22, A115, TOPREAL3:10;
then ex p11 being Point of (TOP-REAL 2) st
( p = p11 & p11 `2 = (f /. i) `2 & (f /. i) `1 <= p11 `1 & p11 `1 <= (f /. (i + 1)) `1 ) ;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A7, A25, A26, A110, A112, FINSEQ_4:67; :: thesis: verum
end;
suppose (f /. (i + 1)) `1 < (f /. i) `1 ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
then p in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `2 = (f /. i) `2 & (f /. (i + 1)) `1 <= p22 `1 & p22 `1 <= (f /. i) `1 ) } by A5, A19, A22, A115, TOPREAL3:10;
then ex p11 being Point of (TOP-REAL 2) st
( p = p11 & p11 `2 = (f /. i) `2 & (f /. (i + 1)) `1 <= p11 `1 & p11 `1 <= (f /. i) `1 ) ;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A7, A25, A26, A110, A112, FINSEQ_4:67; :: thesis: verum
end;
end;
end;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; :: thesis: verum
end;
end;
end;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; :: thesis: verum
end;
suppose A117: n + 1 < len h ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
A118: 1 <= n + 1 by A108, NAT_1:13;
n + 1 <= i by A26, A117, NAT_1:13;
then A119: n + 1 in dom (f | i) by A24, A118, FINSEQ_1:1;
then h /. (n + 1) = (f | i) /. (n + 1) by A7, FINSEQ_4:68;
then A120: h /. (n + 1) = f /. (n + 1) by A119, FINSEQ_4:70;
n <= i by A26, A117, XREAL_1:6;
then A121: n in dom (f | i) by A24, A108, FINSEQ_1:1;
then h /. n = (f | i) /. n by A7, FINSEQ_4:68;
then A122: h /. n = f /. n by A121, FINSEQ_4:70;
n + 1 <= len f by A26, A16, A109, XXREAL_0:2;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A13, A108, A122, A120, TOPREAL1:def 5; :: thesis: verum
end;
end;
end;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; :: thesis: verum
end;
A123: 1 in dom (f | i) by A4, A24, FINSEQ_1:1;
then h /. 1 = (f | i) /. 1 by A7, FINSEQ_4:68
.= f /. 1 by A123, FINSEQ_4:70 ;
hence A124: ( h /. 1 = f /. 1 & h /. (len h) = p ) by A7, A25, A26, FINSEQ_4:67; :: thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
set Mf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
set Mv = { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } ;
set Mh = { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } ;
A125: Seg (len (f | i)) = dom (f | i) by FINSEQ_1:def 3;
thus L~ h is_S-P_arc_joining f /. 1,p by A32, A124, Def1; :: thesis: ( L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
A126: now
let x be set ; :: thesis: ( x in L~ h implies ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) )
assume x in L~ h ; :: thesis: ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
then consider X being set such that
A127: x in X and
A128: X in { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } by TARSKI:def 4;
consider k being Element of NAT such that
A129: X = LSeg (h,k) and
A130: 1 <= k and
A131: k + 1 <= len h by A128;
A132: k + 1 <= len f by A26, A16, A131, XXREAL_0:2;
now
per cases ( k + 1 = len h or k + 1 < len h ) by A131, XXREAL_0:1;
suppose A133: k + 1 = len h ; :: thesis: ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
then A134: LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A26, A16, A130;
LSeg (h,i) c= LSeg (f,i) by A5, A18, A21, A30, TOPREAL1:6;
hence x in L~ f by A26, A127, A129, A133, A134, TARSKI:def 4; :: thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),p))
thus x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) by A26, A30, A127, A129, A133, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A135: k + 1 < len h ; :: thesis: ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
then A136: k + 1 <= len (f | i) by A25, A26, NAT_1:13;
A137: k + 1 <= i by A26, A135, NAT_1:13;
k <= k + 1 by NAT_1:11;
then k <= i by A137, XXREAL_0:2;
then A138: k in dom (f | i) by A24, A130, FINSEQ_1:1;
1 <= k + 1 by A130, NAT_1:13;
then A139: k + 1 in dom (f | i) by A24, A137, FINSEQ_1:1;
then A140: X = LSeg ((f | i),k) by A7, A129, A138, TOPREAL3:18
.= LSeg (f,k) by A139, A138, TOPREAL3:17 ;
then X in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A130, A132;
hence x in L~ f by A127, TARSKI:def 4; :: thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),p))
X = LSeg ((f | i),k) by A139, A138, A140, TOPREAL3:17;
then X in { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A130, A136;
then x in union { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A127, TARSKI:def 4;
hence x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) ; :: thesis: verum
end;
thus L~ h c= L~ f :: thesis: L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p))
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ h or x in L~ f )
assume x in L~ h ; :: thesis: x in L~ f
hence x in L~ f by A126; :: thesis: verum
end;
A141: i <= i + 1 by NAT_1:11;
thus L~ h c= (L~ (f | i)) \/ (LSeg ((f /. i),p)) :: according to XBOOLE_0:def 10 :: thesis: (L~ (f | i)) \/ (LSeg ((f /. i),p)) c= L~ h
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ h or x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
assume x in L~ h ; :: thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),p))
hence x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) by A126; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) or x in L~ h )
assume A142: x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ; :: thesis: x in L~ h
now
per cases ( x in L~ (f | i) or x in LSeg ((f /. i),p) ) by A142, XBOOLE_0:def 3;
suppose x in L~ (f | i) ; :: thesis: x in L~ h
then consider X being set such that
A143: x in X and
A144: X in { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by TARSKI:def 4;
consider k being Element of NAT such that
A145: X = LSeg ((f | i),k) and
A146: 1 <= k and
A147: k + 1 <= len (f | i) by A144;
A148: k + 1 <= len h by A25, A26, A141, A147, XXREAL_0:2;
k <= k + 1 by NAT_1:11;
then k <= len (f | i) by A147, XXREAL_0:2;
then A149: k in Seg (len (f | i)) by A146, FINSEQ_1:1;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (len (f | i)) by A147, FINSEQ_1:1;
then X = LSeg (h,k) by A7, A125, A145, A149, TOPREAL3:18;
then X in { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } by A146, A148;
hence x in L~ h by A143, TARSKI:def 4; :: thesis: verum
end;
suppose A150: x in LSeg ((f /. i),p) ; :: thesis: x in L~ h
LSeg (h,i) in { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } by A4, A26;
hence x in L~ h by A30, A150, TARSKI:def 4; :: thesis: verum
end;
end;
end;
hence x in L~ h ; :: thesis: verum