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 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;

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)) )

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)) )

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

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 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;

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

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 )

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);

end;

A124:
1 in dom (f | i)
by A4, A25, FINSEQ_1:1;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 )

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 )( 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 ;

end;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: contradictionend;

hence
contradiction
; :: thesis: verumper 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;

end;

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

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

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( k2 + 1 = k1 or k2 + 1 < k1 )
by A50, XXREAL_0:1;

end;

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

then A51:
k2 + 1 <= i
by A49, NAT_1:13;

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( k2 + 1 = i or k2 + 1 < i )
by A51, XXREAL_0:1;

end;

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;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

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

then A58:
k2 + 1 <= len f
by A24, XXREAL_0:2;

A59: LSeg (f,k2) misses LSeg (f,i) by A14, A57;

k2 <= k2 + 1 by NAT_1:11;

then k2 <= i by A57, XXREAL_0:2;

then A60: k2 in dom (f | i) by A25, A42, FINSEQ_1:1;

then h /. k2 = (f | i) /. k2 by A7, FINSEQ_4:68

.= f /. k2 by A60, FINSEQ_4:70 ;

then p in LSeg (f,k2) by A27, A28, A42, A44, A49, A58, TOPREAL1:21;

hence contradiction by A5, A59, XBOOLE_0:3; :: thesis: verum

end;A59: LSeg (f,k2) misses LSeg (f,i) by A14, A57;

k2 <= k2 + 1 by NAT_1:11;

then k2 <= i by A57, XXREAL_0:2;

then A60: k2 in dom (f | i) by A25, A42, FINSEQ_1:1;

then h /. k2 = (f | i) /. k2 by A7, FINSEQ_4:68

.= f /. k2 by A60, FINSEQ_4:70 ;

then p in LSeg (f,k2) by A27, A28, A42, A44, A49, A58, TOPREAL1:21;

hence contradiction by A5, A59, XBOOLE_0:3; :: thesis: verum

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

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

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( k1 + 1 = k2 or k1 + 1 < k2 )
by A62, XXREAL_0:1;

end;

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

then A63:
k1 + 1 <= i
by A61, NAT_1:13;

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( k1 + 1 = i or k1 + 1 < i )
by A63, XXREAL_0:1;

end;

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;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

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

then A70:
k1 + 1 <= len f
by A24, XXREAL_0:2;

A71: LSeg (f,k1) misses LSeg (f,i) by A14, A69;

k1 <= k1 + 1 by NAT_1:11;

then k1 <= i by A69, XXREAL_0:2;

then A72: k1 in dom (f | i) by A25, A39, FINSEQ_1:1;

then h /. k1 = (f | i) /. k1 by A7, FINSEQ_4:68

.= f /. k1 by A72, FINSEQ_4:70 ;

then p in LSeg (f,k1) by A27, A28, A39, A44, A61, A70, TOPREAL1:21;

hence contradiction by A5, A71, XBOOLE_0:3; :: thesis: verum

end;A71: LSeg (f,k1) misses LSeg (f,i) by A14, A69;

k1 <= k1 + 1 by NAT_1:11;

then k1 <= i by A69, XXREAL_0:2;

then A72: k1 in dom (f | i) by A25, A39, FINSEQ_1:1;

then h /. k1 = (f | i) /. k1 by A7, FINSEQ_4:68

.= f /. k1 by A72, FINSEQ_4:70 ;

then p in LSeg (f,k1) by A27, A28, A39, A44, A61, A70, TOPREAL1:21;

hence contradiction by A5, A71, XBOOLE_0:3; :: thesis: verum

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;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

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

thus
h is s.n.c.
:: thesis: h is special
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;

end;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))}end;

hence
(LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}
; :: thesis: verumper cases
( j + 2 = len h or j + 2 < len h )
by A77, XXREAL_0:1;

end;

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;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

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;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

proof

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 )
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;

end;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)) = {} end;

hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
; :: according to XBOOLE_0:def 7 :: thesis: verumper cases
( m + 1 < len h or m + 1 = len h or m + 1 > len h )
by XXREAL_0:1;

end;

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 ;

end;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)) = {} end;

hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
; :: thesis: verumper cases
( 0 < n or 0 = n )
;

end;

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;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

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

A106:
(LSeg (f,n)) /\ (LSeg (f,m)) = {}
by A94;

end;now :: thesis: {} = (LSeg (h,n)) /\ (LSeg (h,m))end;

hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
; :: thesis: verumper cases
( 0 < n or 0 = n )
;

end;

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;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

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 )end;

hence
( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
; :: thesis: verumper cases
( n + 1 = len h or n + 1 < len h )
by A110, XXREAL_0:1;

end;

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 ;

end;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 )end;

hence
( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
; :: thesis: verumper cases
( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
by A4, A13, A16;

end;

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;

end;now :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )end;

hence
( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
; :: thesis: verumper cases
( (f /. i) `2 < (f /. (i + 1)) `2 or (f /. (i + 1)) `2 < (f /. i) `2 )
by A115, XXREAL_0:1;

end;

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;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

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;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

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;

end;now :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )end;

hence
( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
; :: thesis: verumper cases
( (f /. i) `1 < (f /. (i + 1)) `1 or (f /. (i + 1)) `1 < (f /. i) `1 )
by A117, XXREAL_0:1;

end;

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;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

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;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

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;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

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)) )

thus
L~ h c= L~ f
by A127; :: thesis: L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p))( 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;

end;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)) )end;

hence
( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) )
; :: thesis: verumper cases
( k + 1 = len h or k + 1 < len h )
by A132, XXREAL_0:1;

end;

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;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

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;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

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~ hend;

hence
x in L~ h
; :: thesis: verumper cases
( x in L~ (f | i) or x in LSeg ((f /. i),p) )
by A143, XBOOLE_0:def 3;

end;

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;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