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