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 p <> f /. 1 & f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg f,i & p <> f /. i & p <> f /. (i + 1) & 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 p <> f /. 1 & f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg f,i & p <> f /. i & p <> f /. (i + 1) & 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: ( p <> f /. 1 & f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg f,i & p <> f /. i & p <> f /. (i + 1) & 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 A1: ( p <> f /. 1 & f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg f,i & p <> f /. i & p <> f /. (i + 1) & 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) )
then A2: f is s.n.c. by TOPREAL1:def 10;
A3: f is unfolded by A1, TOPREAL1:def 10;
A4: f is special by A1, TOPREAL1:def 10;
set v = f | i;
A5: ( f | i = f | (Seg i) & Seg (len f) = dom f & Seg (len h) = dom h & Seg (len (f | i)) = dom (f | i) ) by FINSEQ_1:def 3, FINSEQ_1:def 15;
then A6: ( 1 <= i & i <= len f ) by A1, FINSEQ_1:3;
then ( Seg i c= dom f & dom (f | i) = (dom f) /\ (Seg i) ) by A5, FINSEQ_1:7, RELAT_1:90;
then A7: dom (f | i) = Seg i by XBOOLE_1:28;
then A8: len (f | i) = i by FINSEQ_1:def 3;
then A9: len h = i + (len <*p*>) by A1, FINSEQ_1:35
.= i + 1 by FINSEQ_1:56 ;
A10: 1 in dom (f | i) by A1, A7, FINSEQ_1:3;
then A11: h /. 1 = (f | i) /. 1 by A1, FINSEQ_4:83
.= f /. 1 by A10, FINSEQ_4:85 ;
A12: h /. (len h) = p by A1, A8, A9, FINSEQ_4:82;
set q1 = f /. i;
set q2 = f /. (i + 1);
A13: i + 1 <= len f by A1, A5, FINSEQ_1:3;
then A14: ( LSeg f,i = LSeg (f /. i),(f /. (i + 1)) & f /. i in LSeg (f /. i),(f /. (i + 1)) & p in LSeg (f /. i),(f /. (i + 1)) ) by A1, RLTOPSP1:69, TOPREAL1:def 5;
A15: ( LSeg f,i = LSeg (f /. (i + 1)),(f /. i) & f /. i = |[((f /. i) `1 ),((f /. i) `2 )]| & f /. (i + 1) = |[((f /. (i + 1)) `1 ),((f /. (i + 1)) `2 )]| ) by A1, A13, EUCLID:57, TOPREAL1:def 5;
A16: ( f is one-to-one & i <> i + 1 ) by A1, TOPREAL1:def 10;
then A17: ( f /. i <> f /. (i + 1) & i in dom (f | i) ) by A1, A7, FINSEQ_1:3, PARTFUN2:17;
then A18: h /. i = (f | i) /. i by A1, FINSEQ_4:83
.= f /. i by A17, FINSEQ_4:85 ;
A19: i <= i + 1 by NAT_1:11;
A20: LSeg h,i = LSeg (f /. i),p by A1, A9, A12, A18, TOPREAL1:def 5;
A21: 1 + 1 <= i by A1, NAT_1:13;
thus A22: 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 A23: ( x in dom h & y in dom h & h . x = h . y & x <> y ) ; :: thesis: contradiction
x in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A5, A23, FINSEQ_1:def 1;
then consider k1 being Element of NAT such that
A24: ( k1 = x & 1 <= k1 & k1 <= len h ) ;
y in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A5, A23, FINSEQ_1:def 1;
then consider k2 being Element of NAT such that
A25: ( k2 = y & 1 <= k2 & k2 <= len h ) ;
A26: h /. k1 = h . y by A23, A24, PARTFUN1:def 8
.= h /. k2 by A23, A25, PARTFUN1:def 8 ;
( k1 <= len f & k2 <= len f ) by A9, A13, A24, A25, XXREAL_0:2;
then A27: ( k1 in dom f & k2 in dom f & k2 + (1 + 1) = (k2 + 1) + 1 & k1 + (1 + 1) = (k1 + 1) + 1 ) by A5, A24, A25, FINSEQ_1:3;

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 A9, A24, A25, XXREAL_0:1;

suppose ( k1 = i + 1 & k2 = i + 1 ) ; :: thesis: contradiction

hence contradiction by A23, A24, A25; :: thesis: verum

end;

suppose A28: ( k1 = i + 1 & k2 < i + 1 ) ; :: thesis: contradiction

then A29: k2 + 1 <= k1 by NAT_1:13;

now

per cases ( k2 + 1 = k1 or k2 + 1 < k1 ) by A29, XXREAL_0:1;

suppose k2 + 1 = k1 ; :: thesis: contradiction

hence contradiction by A1, A8, A18, A26, A28, FINSEQ_4:82; :: thesis: verum

end;

suppose k2 + 1 < k1 ; :: thesis: contradiction

then A30: k2 + 1 <= i by A28, NAT_1:13;

now

per cases ( k2 + 1 = i or k2 + 1 < i ) by A30, XXREAL_0:1;

suppose A31: k2 + 1 = i ; :: thesis: contradiction

then A32: (LSeg f,k2) /\ (LSeg f,i) = {(f /. i)} by A3, A13, A25, A27, TOPREAL1:def 8;
k2 + 1 <= len f by A1, A5, A31, FINSEQ_1:3;
then A33: ( f /. k2 in LSeg f,k2 & k2 <= i ) by A25, A31, NAT_1:11, TOPREAL1:27;
then A34: k2 in dom (f | i) by A7, A25, FINSEQ_1:3;
then h /. k2 = (f | i) /. k2 by A1, FINSEQ_4:83
.= f /. k2 by A34, FINSEQ_4:85 ;
then f /. k2 in {(f /. i)} by A1, A9, A12, A26, A28, A32, A33, XBOOLE_0:def 4;
then ( f /. k2 = f /. i & k2 < i ) by A31, NAT_1:13, TARSKI:def 1;
hence contradiction by A1, A16, A27, PARTFUN2:17; :: thesis: verum

end;

suppose A35: k2 + 1 < i ; :: thesis: contradiction

then A36: ( LSeg f,k2 misses LSeg f,i & k2 <= k2 + 1 ) by A2, NAT_1:11, TOPREAL1:def 9;
then k2 <= i by A35, XXREAL_0:2;
then A37: k2 in dom (f | i) by A7, A25, FINSEQ_1:3;
then A38: h /. k2 = (f | i) /. k2 by A1, FINSEQ_4:83
.= f /. k2 by A37, FINSEQ_4:85 ;
k2 + 1 <= len f by A6, A35, XXREAL_0:2;
then p in LSeg f,k2 by A9, A12, A25, A26, A28, A38, TOPREAL1:27;
hence contradiction by A1, A36, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A39: ( k1 < i + 1 & k2 = i + 1 ) ; :: thesis: contradiction

then A40: k1 + 1 <= k2 by NAT_1:13;

now

per cases ( k1 + 1 = k2 or k1 + 1 < k2 ) by A40, XXREAL_0:1;

suppose k1 + 1 = k2 ; :: thesis: contradiction

hence contradiction by A1, A8, A18, A26, A39, FINSEQ_4:82; :: thesis: verum

end;

suppose k1 + 1 < k2 ; :: thesis: contradiction

then A41: k1 + 1 <= i by A39, NAT_1:13;

now

per cases ( k1 + 1 = i or k1 + 1 < i ) by A41, XXREAL_0:1;

suppose A42: k1 + 1 = i ; :: thesis: contradiction

then A43: (LSeg f,k1) /\ (LSeg f,i) = {(f /. i)} by A3, A13, A24, A27, TOPREAL1:def 8;
k1 + 1 <= len f by A1, A5, A42, FINSEQ_1:3;
then A44: ( f /. k1 in LSeg f,k1 & k1 <= i ) by A24, A42, NAT_1:11, TOPREAL1:27;
then A45: k1 in dom (f | i) by A7, A24, FINSEQ_1:3;
then h /. k1 = (f | i) /. k1 by A1, FINSEQ_4:83
.= f /. k1 by A45, FINSEQ_4:85 ;
then f /. k1 in {(f /. i)} by A1, A9, A12, A26, A39, A43, A44, XBOOLE_0:def 4;
then ( f /. k1 = f /. i & k1 < i ) by A42, NAT_1:13, TARSKI:def 1;
hence contradiction by A1, A16, A27, PARTFUN2:17; :: thesis: verum

end;

suppose A46: k1 + 1 < i ; :: thesis: contradiction

then A47: ( LSeg f,k1 misses LSeg f,i & k1 <= k1 + 1 ) by A2, NAT_1:11, TOPREAL1:def 9;
then k1 <= i by A46, XXREAL_0:2;
then A48: k1 in dom (f | i) by A7, A24, FINSEQ_1:3;
then A49: h /. k1 = (f | i) /. k1 by A1, FINSEQ_4:83
.= f /. k1 by A48, FINSEQ_4:85 ;
k1 + 1 <= len f by A6, A46, XXREAL_0:2;
then p in LSeg f,k1 by A9, A12, A24, A26, A39, A49, TOPREAL1:27;
hence contradiction by A1, A47, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose ( k1 < i + 1 & k2 < i + 1 ) ; :: thesis: contradiction

then ( k1 <= i & k2 <= i ) by NAT_1:13;
then A50: ( k1 in dom (f | i) & k2 in dom (f | i) ) by A7, A24, A25, FINSEQ_1:3;
then f . k1 = (f | i) . k1 by A5, FUNCT_1:70
.= h . k1 by A1, A50, FINSEQ_1:def 7
.= (f | i) . k2 by A1, A23, A24, A25, A50, FINSEQ_1:def 7
.= f . k2 by A5, A50, FUNCT_1:70 ;
hence contradiction by A16, A23, A24, A25, A27, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence h is one-to-one by FUNCT_1:def 8; :: according to TOPREAL1:def 10 :: thesis: ( 2 <= len h & h is unfolded & h is s.n.c. & h is special )
thus len h >= 2 by A1, A9, A21, XREAL_1:8; :: 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 8 :: thesis: ( not 1 <= j or not j + 2 <= len h or (LSeg h,j) /\ (LSeg h,(j + 1)) = {(h /. (j + 1))} )
assume A51: ( 1 <= j & j + 2 <= len h ) ; :: thesis: (LSeg h,j) /\ (LSeg h,(j + 1)) = {(h /. (j + 1))}
i + 1 in Seg (len f) by A1, FINSEQ_1:def 3;
then len h <= len f by A9, FINSEQ_1:3;
then A52: j + 2 <= len f by A51, XXREAL_0:2;
then A53: (LSeg f,j) /\ (LSeg f,(j + 1)) = {(f /. (j + 1))} by A3, A51, TOPREAL1:def 8;
(i + 1) + 1 = i + (1 + 1) ;
then len h <= i + 2 by A9, NAT_1:11;
then j + 2 <= i + 2 by A51, XXREAL_0:2;
then A54: j <= i by XREAL_1:8;
(j + 1) + 1 = j + (1 + 1) ;
then A55: ( 1 <= j + 1 & j + 1 <= i ) by A9, A51, NAT_1:11, XREAL_1:8;
then A56: ( j in dom (f | i) & j + 1 in dom (f | i) ) by A7, A51, A54, FINSEQ_1:3;
then A57: LSeg h,j = LSeg (f | i),j by A1, TOPREAL3:25
.= LSeg f,j by A1, A56, TOPREAL3:24 ;
A58: h /. (j + 1) = (f | i) /. (j + 1) by A1, A56, FINSEQ_4:83
.= f /. (j + 1) by A56, FINSEQ_4:85 ;
j <= j + 2 by NAT_1:11;
then A59: 1 <= j + (1 + 1) by A51, XXREAL_0:2;
A60: j + (1 + 1) = (j + 1) + 1 ;

now

per cases ( j + 2 = len h or j + 2 < len h ) by A51, XXREAL_0:1;

suppose j + 2 = len h ; :: thesis: (LSeg h,j) /\ (LSeg h,(j + 1)) = {(h /. (j + 1))}

then A61: (LSeg h,j) /\ (LSeg h,(j + 1)) c= {(h /. (j + 1))} by A9, A14, A20, A53, A57, A58, TOPREAL1:12, XBOOLE_1:26;
j + 1 <= (j + 1) + 1 by NAT_1:11;
then j + 1 <= len h by A51, XXREAL_0:2;
then A62: h /. (j + 1) in LSeg h,j by A51, TOPREAL1:27;
h /. (j + 1) in LSeg h,(j + 1) by A51, A55, A60, TOPREAL1:27;
then h /. (j + 1) in (LSeg h,j) /\ (LSeg h,(j + 1)) by A62, XBOOLE_0:def 4;
then {(h /. (j + 1))} c= (LSeg h,j) /\ (LSeg h,(j + 1)) by ZFMISC_1:37;
hence (LSeg h,j) /\ (LSeg h,(j + 1)) = {(h /. (j + 1))} by A61, 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 A9, NAT_1:13;
then A63: (j + 1) + 1 in dom (f | i) by A7, A59, FINSEQ_1:3;
then LSeg h,(j + 1) = LSeg (f | i),(j + 1) by A1, A56, TOPREAL3:25
.= LSeg f,(j + 1) by A1, A56, A63, TOPREAL3:24 ;
hence (LSeg h,j) /\ (LSeg h,(j + 1)) = {(h /. (j + 1))} by A3, A51, A52, A57, A58, TOPREAL1:def 8; :: 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 9 :: thesis: ( m <= n + 1 or LSeg h,n misses LSeg h,m )
assume A64: m > n + 1 ; :: thesis: LSeg h,n misses LSeg h,m
then ( n + 1 < m & n <= n + 1 ) by NAT_1:11;
then A65: ( n <= m & n + 1 <= m & 1 <= n + 1 & LSeg f,n misses LSeg f,m ) by A2, NAT_1:11, TOPREAL1:def 9, XXREAL_0:2;

now

per cases ( m + 1 < len h or m + 1 = len h or m + 1 > len h ) by XXREAL_0:1;

suppose m + 1 < len h ; :: thesis: (LSeg h,n) /\ (LSeg h,m) = {}

then A66: ( m <= i & m + 1 <= i & m <= m + 1 & 1 < m ) by A9, A64, A65, NAT_1:13, XREAL_1:8, XXREAL_0:2;
then A67: ( m in dom (f | i) & 1 <= m + 1 ) by A7, FINSEQ_1:3, XXREAL_0:2;
then A68: m + 1 in dom (f | i) by A7, A66, FINSEQ_1:3;
then A69: LSeg h,m = LSeg (f | i),m by A1, A67, TOPREAL3:25
.= LSeg f,m by A1, A67, A68, TOPREAL3:24 ;

now

per cases ( 0 < n or 0 = n ) ;

suppose 0 < n ; :: thesis: (LSeg h,n) /\ (LSeg h,m) = {}

then A70: 0 + 1 <= n by NAT_1:13;
( n <= i & n + 1 <= i ) by A65, A66, XXREAL_0:2;
then A71: ( n in dom (f | i) & n + 1 in dom (f | i) ) by A7, A65, A70, FINSEQ_1:3;
then LSeg h,n = LSeg (f | i),n by A1, TOPREAL3:25
.= LSeg f,n by A1, A71, TOPREAL3:24 ;
then LSeg h,n misses LSeg h,m by A2, A64, A69, TOPREAL1:def 9;
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 5;
hence (LSeg h,n) /\ (LSeg h,m) = {} ; :: thesis: verum

end;

end;

end;

hence (LSeg h,n) /\ (LSeg h,m) = {} ; :: thesis: verum

end;

suppose A72: m + 1 = len h ; :: thesis: (LSeg h,n) /\ (LSeg h,m) = {}

A73: (LSeg f,n) /\ (LSeg f,m) = {} by A65, 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 A74: ( n in dom (f | i) & n + 1 in dom (f | i) ) by A7, A9, A65, A72, FINSEQ_1:3;
then LSeg h,n = LSeg (f | i),n by A1, TOPREAL3:25
.= LSeg f,n by A1, A74, TOPREAL3:24 ;
hence {} = (LSeg h,m) /\ ((LSeg f,m) /\ (LSeg h,n)) by A73
.= ((LSeg h,m) /\ (LSeg f,m)) /\ (LSeg h,n) by XBOOLE_1:16
.= (LSeg h,n) /\ (LSeg h,m) by A9, A14, A20, A72, TOPREAL1:12, XBOOLE_1:28 ;
:: thesis: verum

end;

suppose 0 = n ; :: thesis: (LSeg h,n) /\ (LSeg h,m) = {}

then LSeg h,n = {} by TOPREAL1:def 5;
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 5;
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 7 :: 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 A75: ( 1 <= n & 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 A75, XXREAL_0:1;

suppose A76: n + 1 = len h ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )

then A77: ( h /. (n + 1) = p & i in dom (f | i) ) by A1, A5, A8, A9, FINSEQ_1:3, FINSEQ_4:82;
then A78: h /. n = (f | i) /. i by A1, A9, A76, FINSEQ_4:83
.= f /. i by A77, FINSEQ_4:85 ;

now

per cases ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A1, A4, A13, TOPREAL1:def 7;

suppose A79: (f /. i) `1 = (f /. (i + 1)) `1 ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )

then A80: (f /. i) `2 <> (f /. (i + 1)) `2 by A17, TOPREAL3:11;

now

per cases ( (f /. i) `2 < (f /. (i + 1)) `2 or (f /. (i + 1)) `2 < (f /. i) `2 ) by A80, 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 A1, A15, A79, TOPREAL3:15;
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 A1, A8, A9, A76, A78, FINSEQ_4:82; :: 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 A1, A15, A79, TOPREAL3:15;
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 A1, A8, A9, A76, A78, FINSEQ_4:82; :: 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 A81: (f /. i) `2 = (f /. (i + 1)) `2 ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )

then A82: (f /. i) `1 <> (f /. (i + 1)) `1 by A17, TOPREAL3:11;

now

per cases ( (f /. i) `1 < (f /. (i + 1)) `1 or (f /. (i + 1)) `1 < (f /. i) `1 ) by A82, 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 A1, A15, A81, TOPREAL3:16;
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 A1, A8, A9, A76, A78, FINSEQ_4:82; :: 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 A1, A15, A81, TOPREAL3:16;
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 A1, A8, A9, A76, A78, FINSEQ_4:82; :: 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 n + 1 < len h ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )

then ( n <= i & n + 1 <= i & n <= n + 1 ) by A9, NAT_1:13, XREAL_1:8;
then ( n in dom (f | i) & n + 1 <= i & 1 <= n + 1 ) by A7, A75, FINSEQ_1:3, XXREAL_0:2;
then A83: ( n in dom (f | i) & n + 1 in dom (f | i) ) by A7, FINSEQ_1:3;
A84: n + 1 <= len f by A9, A13, A75, XXREAL_0:2;
( h /. n = (f | i) /. n & h /. (n + 1) = (f | i) /. (n + 1) ) by A1, A83, FINSEQ_4:83;
then ( h /. n = f /. n & h /. (n + 1) = f /. (n + 1) ) by A83, FINSEQ_4:85;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A4, A75, A84, TOPREAL1:def 7; :: thesis: verum

end;

end;

end;

hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; :: thesis: verum

end;

thus ( h /. 1 = f /. 1 & h /. (len h) = p ) by A1, A8, A9, A11, FINSEQ_4:82; :: 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) )
hence L~ h is_S-P_arc_joining f /. 1,p by A22, Def1; :: thesis: ( 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 ) } ;

A85: 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
A86: ( x in X & 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
A87: ( X = LSeg h,k & 1 <= k & k + 1 <= len h ) by A86;
A88: k + 1 <= len f by A9, A13, A87, XXREAL_0:2;

now

per cases ( k + 1 = len h or k + 1 < len h ) by A87, XXREAL_0:1;

suppose A89: k + 1 = len h ; :: thesis: ( x in L~ f & x in (L~ (f | i)) \/ (LSeg (f /. i),p) )

then ( k = i & LSeg h,i c= LSeg f,i ) by A9, A14, A20, TOPREAL1:12;
then ( x in LSeg f,k & LSeg f,k in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ) by A13, A86, A87;
hence x in L~ f by TARSKI:def 4; :: thesis: x in (L~ (f | i)) \/ (LSeg (f /. i),p)
thus x in (L~ (f | i)) \/ (LSeg (f /. i),p) by A9, A20, A86, A87, A89, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A90: k + 1 < len h ; :: thesis: ( x in L~ f & x in (L~ (f | i)) \/ (LSeg (f /. i),p) )

then A91: ( k + 1 < i + 1 & k <= k + 1 ) by A9, NAT_1:11;
( k + 1 <= i & 1 <= k + 1 ) by A9, A87, A90, NAT_1:13;
then A92: ( k + 1 in dom (f | i) & k <= i ) by A7, A91, FINSEQ_1:3, XXREAL_0:2;
then A93: k in dom (f | i) by A7, A87, FINSEQ_1:3;
then A94: X = LSeg (f | i),k by A1, A87, A92, TOPREAL3:25
.= LSeg f,k by A1, A92, A93, TOPREAL3:24 ;
then X in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A87, A88;
hence x in L~ f by A86, TARSKI:def 4; :: thesis: x in (L~ (f | i)) \/ (LSeg (f /. i),p)
( X = LSeg (f | i),k & k + 1 <= len (f | i) ) by A1, A8, A9, A90, A92, A93, A94, NAT_1:13, TOPREAL3:24;
then X in { (LSeg (f | i),n) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A87;
then x in union { (LSeg (f | i),n) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A86, 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 A85; :: thesis: verum

end;

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 A85; :: 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 A95: 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 A95, XBOOLE_0:def 3;

suppose x in L~ (f | i) ; :: thesis: x in L~ h

then consider X being set such that
A96: ( x in X & 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
A97: ( X = LSeg (f | i),k & 1 <= k & k + 1 <= len (f | i) ) by A96;
k <= k + 1 by NAT_1:11;
then ( 1 <= k & k <= len (f | i) & 1 <= k + 1 & k + 1 <= len (f | i) ) by A97, XXREAL_0:2;
then A98: ( k in Seg (len (f | i)) & k + 1 in Seg (len (f | i)) ) by FINSEQ_1:3;
A99: k + 1 <= len h by A8, A9, A19, A97, XXREAL_0:2;
X = LSeg h,k by A1, A5, A97, A98, TOPREAL3:25;
then X in { (LSeg h,m) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } by A97, A99;
hence x in L~ h by A96, TARSKI:def 4; :: thesis: verum

end;

suppose A100: 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 A1, A9;
hence x in L~ h by A20, A100, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in L~ h ; :: thesis: verum