let G be Graph; :: thesis:
let vs be FinSequence of the carrier of G; :: thesis:
let c be Chain of G; :: thesis:
assume that
A1: c is not simple Chain of G and
A2: vs is_vertex_seq_of c ; :: thesis:
consider n, m being Nat such that
A3: 1 <= n and
A4: n < m and
A5: m <= len vs and
A6: vs . n = vs . m and
A7: ( n <> 1 or m <> len vs ) by A1, A2, Def9;
A8: m - n > n - n by A4, XREAL_1:9;
A9: len vs = (len c) + 1 by A2;
reconsider n1 = n -' 1 as Element of NAT ;
A10: 1 - 1 <= n - 1 by A3, XREAL_1:9;
then A11: n - 1 = n -' 1 by XREAL_0:def 2;
then A12: n1 + 1 = n ;

per cases by A7;

suppose A13: ( n <> 1 & m <> len vs ) ; :: thesis:

set DR = { kk where kk is Nat : ( m <= kk & kk <= len c ) } ;
set DL = { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } ;
set domfvs = { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ;
reconsider p2 = (m,((len c) + 1)) -cut vs as FinSequence of the carrier of G ;
reconsider pp = (1,n) -cut vs as FinSequence of the carrier of G ;
set p29 = ((m + 1),((len c) + 1)) -cut vs;
A14: 1 <= m + 1 by NAT_1:12;
A15: 1 <= m by A3, A4, XXREAL_0:2;
then 1 - 1 <= m - 1 by XREAL_1:9;
then m -' 1 = m - 1 by XREAL_0:def 2;
then reconsider m1 = m - 1 as Element of NAT ;
A16: m < len vs by A5, A13, XXREAL_0:1;
then A17: m <= len c by A9, NAT_1:13;
then reconsider c2 = (m,(len c)) -cut c as Chain of G by A15, Th41;
A18: (len c2) + m = (len c) + 1 by A15, A17, FINSEQ_6:def 4;
deffunc H₁( object ) -> set = c . $1;
set domfc = { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ;
consider fc being Function such that
A19: dom fc = { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } and
A20: for x being object st x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } holds
fc . x = H₁(x) from FUNCT_1:sch 3();
n < len vs by A4, A5, XXREAL_0:2;
then A21: n - 1 < ((len c) + 1) - 1 by A9, XREAL_1:9;
{ k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } c= Seg (len c)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; :: thesis:
then consider kk being Nat such that
A22: x = kk and
A23: ( ( 1 <= kk & kk <= n1 ) or ( m <= kk & kk <= len c ) ) ;
A24: 1 <= kk by A15, A23, XXREAL_0:2;
kk <= len c by A11, A21, A23, XXREAL_0:2;
hence x in Seg (len c) by A22, A24; :: thesis:

end;

then reconsider fc = fc as FinSubsequence by A19, FINSEQ_1:def 12;
A25: fc c= c

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: p in fc ; :: thesis:
then consider x, y being object such that
A27: [x,y] = p by RELAT_1:def 1;
A28: x in dom fc by A26, A27, FUNCT_1:1;
then consider kk being Nat such that
A29: x = kk and
A30: ( ( 1 <= kk & kk <= n1 ) or ( m <= kk & kk <= len c ) ) by A19;
A31: 1 <= kk by A15, A30, XXREAL_0:2;
kk <= len c by A11, A21, A30, XXREAL_0:2;
then A32: x in dom c by A29, A31, FINSEQ_3:25;
y = fc . x by A26, A27, FUNCT_1:1;
then y = c . kk by A19, A20, A28, A29;
hence p in c by A27, A29, A32, FUNCT_1:1; :: thesis:

end;

1 < n by A3, A13, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then A33: (1 + 1) - 1 <= n - 1 by XREAL_1:9;
then reconsider c1 = (1,n1) -cut c as Chain of G by A11, A21, Th41;
reconsider fc = fc as Subset of c by A25;
take fc ; :: thesis:
A34: pp is_vertex_seq_of c1 by A2, A12, A33, A21, Th42;
then A35: len pp = (len c1) + 1 ;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; :: thesis:
then ex k being Nat st
( x = k & ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) ) ;
then ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } or x in { kk where kk is Nat : ( m <= kk & kk <= len c ) } ) ;
hence x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } by XBOOLE_0:def 3; :: thesis:

end;

assume A36: x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } ; :: thesis:

per cases by A36, XBOOLE_0:def 3;

suppose x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } ; :: thesis:

then ex k being Nat st
( x = k & 1 <= k & k <= n1 ) ;
hence x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; :: thesis:

end;

suppose x in { kk where kk is Nat : ( m <= kk & kk <= len c ) } ; :: thesis:

then ex k being Nat st
( x = k & m <= k & k <= len c ) ;
hence x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; :: thesis:

end;

then A37: { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } = { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } by TARSKI:2;
A38: ( { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } c= Seg (len c) & { kk where kk is Nat : ( m <= kk & kk <= len c ) } c= Seg (len c) )

proof

hereby :: according to TARSKI:def 3 :: thesis:

let x be object ; :: thesis:
assume x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } ; :: thesis:
then consider k being Nat such that
A39: x = k and
A40: 1 <= k and
A41: k <= n1 ;
k <= len c by A11, A21, A41, XXREAL_0:2;
hence x in Seg (len c) by A39, A40; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { kk where kk is Nat : ( m <= kk & kk <= len c ) } ; :: thesis:
then consider k being Nat such that
A42: x = k and
A43: m <= k and
A44: k <= len c ;
1 <= k by A15, A43, XXREAL_0:2;
hence x in Seg (len c) by A42, A44; :: thesis:

end;

then reconsider DR = { kk where kk is Nat : ( m <= kk & kk <= len c ) } as finite set ;
rng (Sgm DR) = DR by A38, FINSEQ_1:def 13;
then A45: rng (Sgm DR) c= dom fc by A19, A37, XBOOLE_1:7;
reconsider DL = { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } as finite set by A38;
set SL = Sgm DL;
A46: 1 <= m by A3, A4, XXREAL_0:2;
set SR = Sgm DR;
A47: len (Sgm DR) = card DR by A38, FINSEQ_3:39;
A48: m <= len c by A9, A16, NAT_1:13;
then A49: m - m <= (len c) - m by XREAL_1:9;
then (len c2) -' 1 = (len c2) - 1 by A18, XREAL_0:def 2;
then reconsider lc21 = (len c2) - 1 as Element of NAT ;
- (- (m - n)) = m - n ;
then A50: - (m - n) < 0 by A8;
A51: m = m1 + 1 ;
then m1 <= m by NAT_1:12;
then A52: p2 = (((m1 + 1),m) -cut vs) ^ (((m + 1),((len c) + 1)) -cut vs) by A5, A9, FINSEQ_6:134;
A53: p2 is_vertex_seq_of c2 by A2, A15, A17, Th42;
then A54: len p2 = (len c2) + 1 ;
then 1 <= len p2 by NAT_1:12;
then 1 - 1 <= (len p2) - 1 by XREAL_1:9;
then (len p2) -' 1 = (len p2) - 1 by XREAL_0:def 2;
then reconsider lp21 = (len p2) - 1 as Element of NAT ;
0 + 1 = 1 ;
then A55: 1 <= len p2 by A54, NAT_1:13;
m - m <= (len c) - m by A48, XREAL_1:9;
then 0 + 1 <= ((len c) - m) + 1 by XREAL_1:6;
then A56: 1 < len p2 by A54, A18, NAT_1:13;
lp21 -' 1 = lp21 - 1 by A54, A18, A49, XREAL_0:def 2;
then reconsider lp22 = lp21 - 1 as Element of NAT ;
A57: (m + 1) + lp22 = m + lp21 ;
m + lc21 = len c by A18;
then A58: card DR = ((len c2) + (- 1)) + 1 by FINSEQ_6:130
.= len c2 ;
A59: m + lc21 = m1 + (len c2) ;

now :: thesis:

let p be object ; :: thesis:

hereby :: thesis:

assume A60: p in c2 ; :: thesis:
then consider x, y being object such that
A61: p = [x,y] by RELAT_1:def 1;
A62: y = c2 . x by A60, A61, FUNCT_1:1;
A63: x in dom c2 by A60, A61, FUNCT_1:1;
then reconsider k = x as Element of NAT ;
A64: k <= len c2 by A63, FINSEQ_3:25;
1 <= k by A63, FINSEQ_3:25;
then A65: m1 + k = (Sgm DR) . k by A51, A18, A59, A64, FINSEQ_6:131;
0 + 1 <= k by A63, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A66: i < len c2 and
A67: k = i + 1 by A64, FINSEQ_6:127;
A68: x in dom (Sgm DR) by A58, A47, A63, FINSEQ_3:29;
then A69: (Sgm DR) . k in rng (Sgm DR) by FUNCT_1:def 3;
then A70: x in dom (fc * (Sgm DR)) by A45, A68, FUNCT_1:11;
then (fc * (Sgm DR)) . x = fc . (m1 + k) by A65, FUNCT_1:12
.= c . (m + i) by A45, A65, A69, A67, GRFUNC_1:2
.= y by A15, A17, A62, A66, A67, FINSEQ_6:def 4 ;
hence p in fc * (Sgm DR) by A61, A70, FUNCT_1:1; :: thesis:

end;

assume A71: p in fc * (Sgm DR) ; :: thesis:
then consider x, y being object such that
A72: p = [x,y] by RELAT_1:def 1;
A73: y = (fc * (Sgm DR)) . x by A71, A72, FUNCT_1:1;
A74: x in dom (fc * (Sgm DR)) by A71, A72, FUNCT_1:1;
then A75: x in dom (Sgm DR) by FUNCT_1:11;
then reconsider k = x as Element of NAT ;
A76: k <= len c2 by A58, A47, A75, FINSEQ_3:25;
1 <= k by A75, FINSEQ_3:25;
then A77: m1 + k = (Sgm DR) . k by A51, A18, A59, A76, FINSEQ_6:131;
A78: k in dom c2 by A58, A47, A75, FINSEQ_3:29;
A79: (Sgm DR) . x in dom fc by A74, FUNCT_1:11;
0 + 1 <= k by A75, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A80: i < len c2 and
A81: k = i + 1 by A76, FINSEQ_6:127;
c2 . k = c . ((m1 + 1) + i) by A15, A17, A80, A81, FINSEQ_6:def 4
.= fc . ((Sgm DR) . k) by A79, A77, A81, GRFUNC_1:2
.= y by A73, A75, FUNCT_1:13 ;
hence p in c2 by A72, A78, FUNCT_1:1; :: thesis:

end;

then A82: c2 = fc * (Sgm DR) by TARSKI:2;

now :: thesis:

let i, j be Nat; :: thesis:
assume i in DL ; :: thesis:
then consider k being Nat such that
A83: k = i and
1 <= k and
A84: k <= n1 ;
assume j in DR ; :: thesis:
then A85: ex l being Nat st
( l = j & m <= l & l <= len c ) ;
n1 < m by A4, A12, NAT_1:13;
then k < m by A84, XXREAL_0:2;
hence i < j by A83, A85, XXREAL_0:2; :: thesis:

end;

then A86: Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR) by A38, FINSEQ_3:42;
set DR = { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ;
A87: 1 <= m + 1 by NAT_1:12;
deffunc H₂( object ) -> set = vs . $1;
consider fvs being Function such that
A88: dom fvs = { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } and
A89: for x being object st x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } holds
fvs . x = H₂(x) from FUNCT_1:sch 3();
A90: n <= len vs by A4, A5, XXREAL_0:2;
{ k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } c= Seg (len vs)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; :: thesis:
then consider kk being Nat such that
A91: x = kk and
A92: ( ( 1 <= kk & kk <= n ) or ( m + 1 <= kk & kk <= len vs ) ) ;
A93: kk <= len vs by A90, A92, XXREAL_0:2;
1 <= m + 1 by NAT_1:12;
then 1 <= kk by A92, XXREAL_0:2;
hence x in Seg (len vs) by A91, A93; :: thesis:

end;

then reconsider fvs = fvs as FinSubsequence by A88, FINSEQ_1:def 12;
fvs c= vs

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A94: p in fvs ; :: thesis:
then consider x, y being object such that
A95: [x,y] = p by RELAT_1:def 1;
A96: x in dom fvs by A94, A95, FUNCT_1:1;
then consider kk being Nat such that
A97: x = kk and
A98: ( ( 1 <= kk & kk <= n ) or ( m + 1 <= kk & kk <= len vs ) ) by A88;
A99: kk <= len vs by A90, A98, XXREAL_0:2;
1 <= m + 1 by NAT_1:12;
then 1 <= kk by A98, XXREAL_0:2;
then A100: x in dom vs by A97, A99, FINSEQ_3:25;
y = fvs . x by A94, A95, FUNCT_1:1;
then y = vs . kk by A88, A89, A96, A97;
hence p in vs by A95, A97, A100, FUNCT_1:1; :: thesis:

end;

then reconsider fvs = fvs as Subset of vs ;
A101: (len c) + 1 <= len vs by A2;
A102: m <= (len c) + 1 by A2, A5;
then A103: p2 . 1 = vs . m by A46, A101, FINSEQ_6:138;
A104: pp . (len pp) = vs . n by A3, A90, FINSEQ_6:138;
then reconsider c9 = c1 ^ c2 as Chain of G by A6, A34, A53, A103, Th43;
take fvs ; :: thesis:
take c9 ; :: thesis:
take p1 = pp ^' p2; :: thesis:
A105: 1 <= n1 + 1 by NAT_1:12;
then A106: (len c1) + 1 = n1 + 1 by A11, A21, Lm2;
then len c1 = n - 1 by A10, XREAL_0:def 2;
then len c9 = (n + (- 1)) + ((len c) + ((- m) + 1)) by A18, FINSEQ_1:22
.= (len c) + (n + (- m)) ;
hence A107: len c9 < len c by A50, XREAL_1:30; :: thesis:
A108: Sgm DL = idseq n1 by FINSEQ_3:48;
then A109: dom (Sgm DL) = Seg n1 ;

now :: thesis:

let p be object ; :: thesis:

hereby :: thesis:

assume A110: p in c1 ; :: thesis:
then consider x, y being object such that
A111: p = [x,y] by RELAT_1:def 1;
A112: y = c1 . x by A110, A111, FUNCT_1:1;
A113: x in dom c1 by A110, A111, FUNCT_1:1;
then reconsider k = x as Element of NAT ;
A114: k <= len c1 by A113, FINSEQ_3:25;
A115: 1 <= k by A113, FINSEQ_3:25;
then A116: k in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } by A106, A114;
0 + 1 <= k by A113, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A117: i < n1 and
A118: k = i + 1 by A106, A114, FINSEQ_6:127;
A119: x in dom (Sgm DL) by A106, A109, A115, A114;
then A120: k = (Sgm DL) . k by A108, FUNCT_1:18;
then A121: x in dom (fc * (Sgm DL)) by A19, A119, A116, FUNCT_1:11;
then (fc * (Sgm DL)) . x = fc . k by A120, FUNCT_1:12
.= c . (1 + i) by A19, A116, A118, GRFUNC_1:2
.= y by A11, A21, A105, A106, A112, A117, A118, Lm2 ;
hence p in fc * (Sgm DL) by A111, A121, FUNCT_1:1; :: thesis:

end;

assume A122: p in fc * (Sgm DL) ; :: thesis:
then consider x, y being object such that
A123: p = [x,y] by RELAT_1:def 1;
A124: y = (fc * (Sgm DL)) . x by A122, A123, FUNCT_1:1;
A125: x in dom (fc * (Sgm DL)) by A122, A123, FUNCT_1:1;
then A126: (fc * (Sgm DL)) . x = fc . ((Sgm DL) . x) by FUNCT_1:12;
A127: x in dom (Sgm DL) by A125, FUNCT_1:11;
then consider k being Nat such that
A128: k = x and
A129: 1 <= k and
A130: k <= n1 by A109;
A131: k in dom fc by A19, A129, A130;
A132: k in dom c1 by A106, A129, A130, FINSEQ_3:25;
A133: k = (Sgm DL) . k by A108, A127, A128, FUNCT_1:18;
0 + 1 <= k by A129;
then ex i being Nat st
( 0 <= i & i < n1 & k = i + 1 ) by A130, FINSEQ_6:127;
then c1 . k = c . k by A11, A21, A105, A106, Lm2
.= y by A124, A126, A128, A131, A133, GRFUNC_1:2 ;
hence p in c1 by A123, A128, A132, FUNCT_1:1; :: thesis:

end;

then A134: c1 = fc * (Sgm DL) by TARSKI:2;
thus p1 is_vertex_seq_of c9 by A6, A34, A53, A103, A104, Th44; :: thesis:
then len p1 = (len c9) + 1 ;
hence len p1 < len vs by A9, A107, XREAL_1:6; :: thesis:
1 <= 1 + (len c1) by NAT_1:12;
then 1 <= len pp by A34;
then p1 . 1 = pp . 1 by FINSEQ_6:140;
hence vs . 1 = p1 . 1 by A3, A90, FINSEQ_6:138; :: thesis:
p2 . (len p2) = vs . ((len c) + 1) by A46, A102, A101, FINSEQ_6:138;
hence vs . (len vs) = p1 . (len p1) by A9, A56, FINSEQ_6:142; :: thesis:
A135: p2 = ((0 + 1),(len p2)) -cut p2 by FINSEQ_6:133
.= (((0 + 1),1) -cut p2) ^ (((1 + 1),(len p2)) -cut p2) by A55, FINSEQ_6:134 ;
rng (Sgm DL) = DL by A38, FINSEQ_1:def 13;
then rng (Sgm DL) c= dom fc by A19, A37, XBOOLE_1:7;
hence Seq fc = c9 by A19, A37, A86, A45, A134, A82, FINSEQ_6:150; :: thesis:
set DL = { kk where kk is Nat : ( 1 <= kk & kk <= n ) } ;
A136: ( { kk where kk is Nat : ( 1 <= kk & kk <= n ) } c= Seg (len vs) & { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } c= Seg (len vs) )

proof

hereby :: according to TARSKI:def 3 :: thesis:

let x be object ; :: thesis:
assume x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } ; :: thesis:
then consider k being Nat such that
A137: x = k and
A138: 1 <= k and
A139: k <= n ;
k <= len vs by A90, A139, XXREAL_0:2;
hence x in Seg (len vs) by A137, A138; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ; :: thesis:
then consider k being Nat such that
A140: x = k and
A141: m + 1 <= k and
A142: k <= len vs ;
1 <= m + 1 by NAT_1:12;
then 1 <= k by A141, XXREAL_0:2;
hence x in Seg (len vs) by A140, A142; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; :: thesis:
then ex k being Nat st
( x = k & ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) ) ;
then ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } or x in { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ) ;
hence x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } by XBOOLE_0:def 3; :: thesis:

end;

assume A143: x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ; :: thesis:

per cases by A143, XBOOLE_0:def 3;

suppose x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } ; :: thesis:

then ex k being Nat st
( x = k & 1 <= k & k <= n ) ;
hence x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; :: thesis:

end;

suppose x in { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ; :: thesis:

then ex k being Nat st
( x = k & m + 1 <= k & k <= len vs ) ;
hence x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; :: thesis:

end;

then A144: { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } = { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } by TARSKI:2;
reconsider DR = { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } as finite set by A136;
rng (Sgm DR) = DR by A136, FINSEQ_1:def 13;
then A145: rng (Sgm DR) c= dom fvs by A88, A144, XBOOLE_1:7;
reconsider DL = { kk where kk is Nat : ( 1 <= kk & kk <= n ) } as finite set by A136;
A146: m + 1 <= ((len c) + 1) + 1 by A5, A9, XREAL_1:6;
A147: m <= ((len c) + 1) + 1 by A5, A9, NAT_1:12;
then A148: (len p2) + m = ((len c) + 1) + 1 by A9, A15, Lm2
.= (len (((m + 1),((len c) + 1)) -cut vs)) + (m + 1) by A9, A14, A146, Lm2
.= ((len (((m + 1),((len c) + 1)) -cut vs)) + 1) + m ;
set SL = Sgm DL;
A149: Sgm DL = idseq n by FINSEQ_3:48;
then A150: dom (Sgm DL) = Seg n ;

now :: thesis:

let p be object ; :: thesis:

hereby :: thesis:

assume A151: p in pp ; :: thesis:
then consider x, y being object such that
A152: p = [x,y] by RELAT_1:def 1;
A153: y = pp . x by A151, A152, FUNCT_1:1;
A154: x in dom pp by A151, A152, FUNCT_1:1;
then reconsider k = x as Element of NAT ;
A155: k <= len pp by A154, FINSEQ_3:25;
A156: 1 <= k by A154, FINSEQ_3:25;
then A157: k in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } by A11, A35, A106, A155;
0 + 1 <= k by A154, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A158: i < n and
A159: k = i + 1 by A11, A35, A106, A155, FINSEQ_6:127;
A160: x in dom (Sgm DL) by A11, A35, A106, A150, A156, A155;
then A161: k = (Sgm DL) . k by A149, FUNCT_1:18;
then A162: x in dom (fvs * (Sgm DL)) by A88, A160, A157, FUNCT_1:11;
then (fvs * (Sgm DL)) . x = fvs . k by A161, FUNCT_1:12
.= vs . (1 + i) by A88, A157, A159, GRFUNC_1:2
.= y by A3, A11, A90, A35, A106, A153, A158, A159, FINSEQ_6:def 4 ;
hence p in fvs * (Sgm DL) by A152, A162, FUNCT_1:1; :: thesis:

end;

assume A163: p in fvs * (Sgm DL) ; :: thesis:
then consider x, y being object such that
A164: p = [x,y] by RELAT_1:def 1;
A165: y = (fvs * (Sgm DL)) . x by A163, A164, FUNCT_1:1;
A166: x in dom (fvs * (Sgm DL)) by A163, A164, FUNCT_1:1;
then A167: (fvs * (Sgm DL)) . x = fvs . ((Sgm DL) . x) by FUNCT_1:12;
A168: x in dom (Sgm DL) by A166, FUNCT_1:11;
then consider k being Nat such that
A169: k = x and
A170: 1 <= k and
A171: k <= n by A150;
A172: k in dom fvs by A88, A170, A171;
A173: k = (Sgm DL) . k by A149, A168, A169, FUNCT_1:18;
A174: k in dom pp by A11, A35, A106, A170, A171, FINSEQ_3:25;
0 + 1 <= k by A170;
then ex i being Nat st
( 0 <= i & i < n & k = i + 1 ) by A171, FINSEQ_6:127;
then pp . k = vs . k by A3, A11, A90, A35, A106, FINSEQ_6:def 4
.= y by A165, A167, A169, A172, A173, GRFUNC_1:2 ;
hence p in pp by A164, A169, A174, FUNCT_1:1; :: thesis:

end;

then A175: pp = fvs * (Sgm DL) by TARSKI:2;
set SR = Sgm DR;
A176: len (Sgm DR) = card DR by A136, FINSEQ_3:39;
A177: (m + 1) + lp22 = m + ((lp21 - 1) + 1)
.= m + (((((len c) - m) + 1) + 1) - 1) by A53, A18
.= (len c) + 1 ;
then A178: card DR = (lp21 - 1) + 1 by A9, FINSEQ_6:130
.= lp21 ;
A179: m + 1 <= ((len c) + 1) + 1 by A5, A9, XREAL_1:7;

now :: thesis:

let p be object ; :: thesis:

hereby :: thesis:

assume A180: p in ((m + 1),((len c) + 1)) -cut vs ; :: thesis:
then consider x, y being object such that
A181: p = [x,y] by RELAT_1:def 1;
A182: y = (((m + 1),((len c) + 1)) -cut vs) . x by A180, A181, FUNCT_1:1;
A183: x in dom (((m + 1),((len c) + 1)) -cut vs) by A180, A181, FUNCT_1:1;
then reconsider k = x as Element of NAT ;
A184: k <= len (((m + 1),((len c) + 1)) -cut vs) by A183, FINSEQ_3:25;
1 <= k by A183, FINSEQ_3:25;
then A185: m + k = (Sgm DR) . k by A9, A177, A148, A57, A184, FINSEQ_6:131;
0 + 1 <= k by A183, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A186: i < len (((m + 1),((len c) + 1)) -cut vs) and
A187: k = i + 1 by A184, FINSEQ_6:127;
A188: x in dom (Sgm DR) by A178, A148, A176, A183, FINSEQ_3:29;
then A189: (Sgm DR) . k in rng (Sgm DR) by FUNCT_1:def 3;
then A190: x in dom (fvs * (Sgm DR)) by A145, A188, FUNCT_1:11;
then (fvs * (Sgm DR)) . x = fvs . (m + k) by A185, FUNCT_1:12
.= vs . ((m + 1) + i) by A145, A185, A189, A187, GRFUNC_1:2
.= y by A9, A87, A179, A182, A186, A187, Lm2 ;
hence p in fvs * (Sgm DR) by A181, A190, FUNCT_1:1; :: thesis:

end;

assume A191: p in fvs * (Sgm DR) ; :: thesis:
then consider x, y being object such that
A192: p = [x,y] by RELAT_1:def 1;
A193: y = (fvs * (Sgm DR)) . x by A191, A192, FUNCT_1:1;
A194: x in dom (fvs * (Sgm DR)) by A191, A192, FUNCT_1:1;
then A195: x in dom (Sgm DR) by FUNCT_1:11;
then reconsider k = x as Element of NAT ;
A196: k <= len (((m + 1),((len c) + 1)) -cut vs) by A178, A148, A176, A195, FINSEQ_3:25;
1 <= k by A195, FINSEQ_3:25;
then A197: m + k = (Sgm DR) . k by A9, A177, A148, A57, A196, FINSEQ_6:131;
A198: k in dom (((m + 1),((len c) + 1)) -cut vs) by A178, A148, A176, A195, FINSEQ_3:29;
A199: (Sgm DR) . x in dom fvs by A194, FUNCT_1:11;
0 + 1 <= k by A195, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A200: i < len (((m + 1),((len c) + 1)) -cut vs) and
A201: k = i + 1 by A196, FINSEQ_6:127;
(((m + 1),((len c) + 1)) -cut vs) . k = vs . ((m + 1) + i) by A9, A87, A179, A200, A201, Lm2
.= fvs . ((Sgm DR) . k) by A199, A197, A201, GRFUNC_1:2
.= y by A193, A195, FUNCT_1:13 ;
hence p in ((m + 1),((len c) + 1)) -cut vs by A192, A198, FUNCT_1:1; :: thesis:

end;

then A202: ((m + 1),((len c) + 1)) -cut vs = fvs * (Sgm DR) by TARSKI:2;

now :: thesis:

let i, j be Nat; :: thesis:
assume i in DL ; :: thesis:
then consider k being Nat such that
A203: k = i and
1 <= k and
A204: k <= n ;
A205: k < m by A4, A204, XXREAL_0:2;
assume j in DR ; :: thesis:
then consider l being Nat such that
A206: l = j and
A207: m + 1 <= l and
l <= len vs ;
m <= m + 1 by NAT_1:12;
then m <= l by A207, XXREAL_0:2;
hence i < j by A203, A206, A205, XXREAL_0:2; :: thesis:

end;

then A208: Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR) by A136, FINSEQ_3:42;
(1,1) -cut p2 = <*(p2 . (0 + 1))*> by A55, FINSEQ_6:132
.= <*(vs . (m + 0))*> by A9, A15, A54, A147, Lm2
.= (m,m) -cut vs by A5, A15, FINSEQ_6:132 ;
then A209: p1 = pp ^ (((m + 1),((len c) + 1)) -cut vs) by A135, A52, FINSEQ_1:33;
rng (Sgm DL) = DL by A136, FINSEQ_1:def 13;
then rng (Sgm DL) c= dom fvs by A88, A144, XBOOLE_1:7;
hence Seq fvs = p1 by A88, A209, A144, A208, A145, A175, A202, FINSEQ_6:150; :: thesis:

end;

suppose A210: ( n = 1 & m <> len vs ) ; :: thesis:

set domfvs = { k where k is Nat : ( m <= k & k <= len vs ) } ;
deffunc H₁( object ) -> set = c . $1;
set domfc = { k where k is Nat : ( m <= k & k <= len c ) } ;
set p2 = (m,((len c) + 1)) -cut vs;
consider fc being Function such that
A211: dom fc = { k where k is Nat : ( m <= k & k <= len c ) } and
A212: for x being object st x in { k where k is Nat : ( m <= k & k <= len c ) } holds
fc . x = H₁(x) from FUNCT_1:sch 3();
A213: 1 < m by A3, A4, XXREAL_0:2;
then 1 - 1 < m - 1 by XREAL_1:9;
then 0 < - (- (m - 1)) ;
then A214: - (m - 1) < 0 ;
1 - 1 <= m - 1 by A213, XREAL_1:9;
then m -' 1 = m - 1 by XREAL_0:def 2;
then reconsider m1 = m - 1 as Element of NAT ;
A215: m = m1 + 1 ;
{ k where k is Nat : ( m <= k & k <= len c ) } c= Seg (len c)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Nat : ( m <= k & k <= len c ) } ; :: thesis:
then consider kk being Nat such that
A216: x = kk and
A217: m <= kk and
A218: kk <= len c ;
1 <= kk by A213, A217, XXREAL_0:2;
hence x in Seg (len c) by A216, A218; :: thesis:

end;

then reconsider fc = fc as FinSubsequence by A211, FINSEQ_1:def 12;
fc c= c

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A219: p in fc ; :: thesis:
then consider x, y being object such that
A220: [x,y] = p by RELAT_1:def 1;
A221: x in dom fc by A219, A220, FUNCT_1:1;
then consider kk being Nat such that
A222: x = kk and
A223: m <= kk and
A224: kk <= len c by A211;
1 <= kk by A213, A223, XXREAL_0:2;
then A225: x in dom c by A222, A224, FINSEQ_3:25;
y = fc . x by A219, A220, FUNCT_1:1;
then y = c . kk by A211, A212, A221, A222;
hence p in c by A220, A222, A225, FUNCT_1:1; :: thesis:

end;

then reconsider fc = fc as Subset of c ;
take fc ; :: thesis:
deffunc H₂( object ) -> set = vs . $1;
consider fvs being Function such that
A226: dom fvs = { k where k is Nat : ( m <= k & k <= len vs ) } and
A227: for x being object st x in { k where k is Nat : ( m <= k & k <= len vs ) } holds
fvs . x = H₂(x) from FUNCT_1:sch 3();
{ k where k is Nat : ( m <= k & k <= len vs ) } c= Seg (len vs)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Nat : ( m <= k & k <= len vs ) } ; :: thesis:
then consider kk being Nat such that
A228: x = kk and
A229: m <= kk and
A230: kk <= len vs ;
1 <= kk by A213, A229, XXREAL_0:2;
hence x in Seg (len vs) by A228, A230; :: thesis:

end;

then reconsider fvs = fvs as FinSubsequence by A226, FINSEQ_1:def 12;
A231: fvs c= vs

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A232: p in fvs ; :: thesis:
then consider x, y being object such that
A233: [x,y] = p by RELAT_1:def 1;
A234: x in dom fvs by A232, A233, FUNCT_1:1;
then consider kk being Nat such that
A235: x = kk and
A236: m <= kk and
A237: kk <= len vs by A226;
1 <= kk by A213, A236, XXREAL_0:2;
then A238: x in dom vs by A235, A237, FINSEQ_3:25;
y = fvs . x by A232, A233, FUNCT_1:1;
then y = vs . kk by A226, A227, A234, A235;
hence p in vs by A233, A235, A238, FUNCT_1:1; :: thesis:

end;

A239: m < len vs by A5, A210, XXREAL_0:1;
then A240: m <= len c by A9, NAT_1:13;
then reconsider c2 = (m,(len c)) -cut c as Chain of G by A213, Th41;
A241: m <= len c by A9, A239, NAT_1:13;
reconsider fvs = fvs as Subset of vs by A231;
take fvs ; :: thesis:
take c1 = c2; :: thesis:
take p1 = (m,((len c) + 1)) -cut vs; :: thesis:
A242: (len c2) + m = (len c) + 1 by A4, A5, A9, A210, Lm2;
then len c2 = (len c) + ((- m) + 1) ;
hence A243: len c1 < len c by A214, XREAL_1:30; :: thesis:
1 <= m by A3, A4, XXREAL_0:2;
hence p1 is_vertex_seq_of c1 by A2, A241, Th42; :: thesis:
(m,((len c) + 1)) -cut vs is_vertex_seq_of c2 by A2, A240, A213, Th42;
then len p1 = (len c1) + 1 ;
hence len p1 < len vs by A9, A243, XREAL_1:6; :: thesis:
thus vs . 1 = p1 . 1 by A4, A5, A6, A9, A210, FINSEQ_6:138; :: thesis:
thus vs . (len vs) = p1 . (len p1) by A4, A5, A9, A210, FINSEQ_6:138; :: thesis:
A244: { k where k is Nat : ( m <= k & k <= len vs ) } c= Seg (len vs)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Nat : ( m <= k & k <= len vs ) } ; :: thesis:
then consider k being Nat such that
A245: x = k and
A246: m <= k and
A247: k <= len vs ;
1 <= k by A213, A246, XXREAL_0:2;
hence x in Seg (len vs) by A245, A247; :: thesis:

end;

A248: { k where k is Nat : ( m <= k & k <= len c ) } c= Seg (len c)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Nat : ( m <= k & k <= len c ) } ; :: thesis:
then consider k being Nat such that
A249: x = k and
A250: m <= k and
A251: k <= len c ;
1 <= k by A213, A250, XXREAL_0:2;
hence x in Seg (len c) by A249, A251; :: thesis:

end;

then reconsider domfc = { k where k is Nat : ( m <= k & k <= len c ) } as finite set ;
A252: len (Sgm domfc) = card domfc by A248, FINSEQ_3:39;
reconsider domfvs = { k where k is Nat : ( m <= k & k <= len vs ) } as finite set by A244;
A253: rng (Sgm domfvs) c= dom fvs by A226, A244, FINSEQ_1:def 13;
set SR = Sgm domfc;
A254: (len c) + 1 <= len vs by A2;
A255: m - m <= (len c) - m by A240, XREAL_1:9;
then (len c2) -' 1 = (len c2) - 1 by A242, XREAL_0:def 2;
then reconsider lc21 = (len c2) - 1 as Element of NAT ;
A256: m + lc21 = m1 + (len c2) ;
(len c2) -' 1 = (len c2) - 1 by A242, A255, XREAL_0:def 2;
then reconsider lc21 = (len c2) - 1 as Element of NAT ;
m + lc21 = len c by A242;
then A257: card domfc = ((len c2) + (- 1)) + 1 by FINSEQ_6:130
.= len c2 ;
A258: rng (Sgm domfc) c= dom fc by A211, A248, FINSEQ_1:def 13;

now :: thesis:

let p be object ; :: thesis:

hereby :: thesis:

assume A259: p in c2 ; :: thesis:
then consider x, y being object such that
A260: p = [x,y] by RELAT_1:def 1;
A261: y = c2 . x by A259, A260, FUNCT_1:1;
A262: x in dom c2 by A259, A260, FUNCT_1:1;
then reconsider k = x as Element of NAT ;
A263: k <= len c2 by A262, FINSEQ_3:25;
1 <= k by A262, FINSEQ_3:25;
then A264: m1 + k = (Sgm domfc) . k by A242, A215, A256, A263, FINSEQ_6:131;
0 + 1 <= k by A262, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A265: i < len c2 and
A266: k = i + 1 by A263, FINSEQ_6:127;
A267: x in dom (Sgm domfc) by A257, A252, A262, FINSEQ_3:29;
then A268: (Sgm domfc) . k in rng (Sgm domfc) by FUNCT_1:def 3;
then A269: x in dom (fc * (Sgm domfc)) by A258, A267, FUNCT_1:11;
then (fc * (Sgm domfc)) . x = fc . (m1 + k) by A264, FUNCT_1:12
.= c . (m + i) by A258, A264, A268, A266, GRFUNC_1:2
.= y by A4, A5, A9, A210, A261, A265, A266, Lm2 ;
hence p in fc * (Sgm domfc) by A260, A269, FUNCT_1:1; :: thesis:

end;

assume A270: p in fc * (Sgm domfc) ; :: thesis:
then consider x, y being object such that
A271: p = [x,y] by RELAT_1:def 1;
A272: y = (fc * (Sgm domfc)) . x by A270, A271, FUNCT_1:1;
A273: x in dom (fc * (Sgm domfc)) by A270, A271, FUNCT_1:1;
then A274: x in dom (Sgm domfc) by FUNCT_1:11;
then reconsider k = x as Element of NAT ;
A275: k <= len c2 by A257, A252, A274, FINSEQ_3:25;
1 <= k by A274, FINSEQ_3:25;
then A276: m1 + k = (Sgm domfc) . k by A242, A215, A256, A275, FINSEQ_6:131;
A277: k in dom c2 by A257, A252, A274, FINSEQ_3:29;
A278: (Sgm domfc) . x in dom fc by A273, FUNCT_1:11;
0 + 1 <= k by A274, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A279: i < len c2 and
A280: k = i + 1 by A275, FINSEQ_6:127;
c2 . k = c . ((m1 + 1) + i) by A4, A5, A9, A210, A279, A280, Lm2
.= fc . ((Sgm domfc) . k) by A278, A276, A280, GRFUNC_1:2
.= y by A272, A274, FUNCT_1:13 ;
hence p in c2 by A271, A277, FUNCT_1:1; :: thesis:

end;

hence Seq fc = c1 by A211, TARSKI:2; :: thesis:
set SR = Sgm domfvs;
A281: len (Sgm domfvs) = card domfvs by A244, FINSEQ_3:39;
A282: m <= ((len c) + 1) + 1 by A5, A9, NAT_1:12;
then A283: (len ((m,((len c) + 1)) -cut vs)) + m = ((len c) + 1) + 1 by A4, A210, A254, Lm2;
then len ((m,((len c) + 1)) -cut vs) = (((len c) - m) + 1) + 1 ;
then 1 <= len ((m,((len c) + 1)) -cut vs) by A242, NAT_1:12;
then 1 - 1 <= (len ((m,((len c) + 1)) -cut vs)) - 1 by XREAL_1:9;
then (len ((m,((len c) + 1)) -cut vs)) -' 1 = (len ((m,((len c) + 1)) -cut vs)) - 1 by XREAL_0:def 2;
then reconsider lp21 = (len ((m,((len c) + 1)) -cut vs)) - 1 as Element of NAT ;
m + lp21 = (len c) + 1 by A283;
then A284: card domfvs = ((len ((m,((len c) + 1)) -cut vs)) + (- 1)) + 1 by A9, FINSEQ_6:130
.= len ((m,((len c) + 1)) -cut vs) ;
A285: m + lp21 = m1 + (len ((m,((len c) + 1)) -cut vs)) ;

now :: thesis:

let p be object ; :: thesis:

hereby :: thesis:

assume A286: p in (m,((len c) + 1)) -cut vs ; :: thesis:
then consider x, y being object such that
A287: p = [x,y] by RELAT_1:def 1;
A288: y = ((m,((len c) + 1)) -cut vs) . x by A286, A287, FUNCT_1:1;
A289: x in dom ((m,((len c) + 1)) -cut vs) by A286, A287, FUNCT_1:1;
then reconsider k = x as Element of NAT ;
A290: k <= len ((m,((len c) + 1)) -cut vs) by A289, FINSEQ_3:25;
1 <= k by A289, FINSEQ_3:25;
then A291: m1 + k = (Sgm domfvs) . k by A9, A215, A283, A285, A290, FINSEQ_6:131;
0 + 1 <= k by A289, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A292: i < len ((m,((len c) + 1)) -cut vs) and
A293: k = i + 1 by A290, FINSEQ_6:127;
A294: x in dom (Sgm domfvs) by A284, A281, A289, FINSEQ_3:29;
then A295: (Sgm domfvs) . k in rng (Sgm domfvs) by FUNCT_1:def 3;
then A296: x in dom (fvs * (Sgm domfvs)) by A253, A294, FUNCT_1:11;
then (fvs * (Sgm domfvs)) . x = fvs . (m1 + k) by A291, FUNCT_1:12
.= vs . (m + i) by A253, A291, A295, A293, GRFUNC_1:2
.= y by A4, A210, A282, A254, A288, A292, A293, Lm2 ;
hence p in fvs * (Sgm domfvs) by A287, A296, FUNCT_1:1; :: thesis:

end;

assume A297: p in fvs * (Sgm domfvs) ; :: thesis:
then consider x, y being object such that
A298: p = [x,y] by RELAT_1:def 1;
A299: y = (fvs * (Sgm domfvs)) . x by A297, A298, FUNCT_1:1;
A300: x in dom (fvs * (Sgm domfvs)) by A297, A298, FUNCT_1:1;
then A301: x in dom (Sgm domfvs) by FUNCT_1:11;
then reconsider k = x as Element of NAT ;
A302: k <= len ((m,((len c) + 1)) -cut vs) by A284, A281, A301, FINSEQ_3:25;
1 <= k by A301, FINSEQ_3:25;
then A303: m1 + k = (Sgm domfvs) . k by A9, A215, A283, A285, A302, FINSEQ_6:131;
A304: k in dom ((m,((len c) + 1)) -cut vs) by A284, A281, A301, FINSEQ_3:29;
A305: (Sgm domfvs) . x in dom fvs by A300, FUNCT_1:11;
0 + 1 <= k by A301, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A306: i < len ((m,((len c) + 1)) -cut vs) and
A307: k = i + 1 by A302, FINSEQ_6:127;
((m,((len c) + 1)) -cut vs) . k = vs . ((m1 + 1) + i) by A4, A210, A282, A254, A306, A307, Lm2
.= fvs . ((Sgm domfvs) . k) by A305, A303, A307, GRFUNC_1:2
.= y by A299, A301, FUNCT_1:13 ;
hence p in (m,((len c) + 1)) -cut vs by A298, A304, FUNCT_1:1; :: thesis:

end;

hence Seq fvs = p1 by A226, TARSKI:2; :: thesis:

end;

suppose A308: ( n <> 1 & m = len vs ) ; :: thesis:

set domfvs = { k where k is Nat : ( 1 <= k & k <= n ) } ;
set pp = (1,n) -cut vs;
deffunc H₁( object ) -> set = c . $1;
reconsider domfc = { k where k is Nat : ( 1 <= k & k <= n1 ) } as set ;
consider fc being Function such that
A309: dom fc = domfc and
A310: for x being object st x in domfc holds
fc . x = H₁(x) from FUNCT_1:sch 3();
n < len vs by A4, A5, XXREAL_0:2;
then A311: n - 1 < ((len c) + 1) - 1 by A9, XREAL_1:9;
domfc c= Seg (len c)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in domfc ; :: thesis:
then consider kk being Nat such that
A312: x = kk and
A313: 1 <= kk and
A314: kk <= n1 ;
kk <= len c by A11, A311, A314, XXREAL_0:2;
hence x in Seg (len c) by A312, A313; :: thesis:

end;

then reconsider fc = fc as FinSubsequence by A309, FINSEQ_1:def 12;
1 < n by A3, A308, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then A315: (1 + 1) - 1 <= n - 1 by XREAL_1:9;
then reconsider c1 = (1,n1) -cut c as Chain of G by A11, A311, Th41;
A316: 1 <= n1 + 1 by NAT_1:12;
then A317: (len c1) + 1 = n1 + 1 by A11, A311, Lm2;
then A318: len c1 = n - 1 by A10, XREAL_0:def 2;
A319: fc c= c

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A320: p in fc ; :: thesis:
then consider x, y being object such that
A321: [x,y] = p by RELAT_1:def 1;
A322: x in dom fc by A320, A321, FUNCT_1:1;
then consider kk being Nat such that
A323: x = kk and
A324: 1 <= kk and
A325: kk <= n1 by A309;
kk <= len c by A11, A311, A325, XXREAL_0:2;
then A326: x in dom c by A323, A324, FINSEQ_3:25;
y = fc . x by A320, A321, FUNCT_1:1;
then y = c . kk by A309, A310, A322, A323;
hence p in c by A321, A323, A326, FUNCT_1:1; :: thesis:

end;

A327: domfc c= Seg (len c)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in domfc ; :: thesis:
then consider k being Nat such that
A328: x = k and
A329: 1 <= k and
A330: k <= n1 ;
k <= len c by A11, A311, A330, XXREAL_0:2;
hence x in Seg (len c) by A328, A329; :: thesis:

end;

reconsider fc = fc as Subset of c by A319;
take fc ; :: thesis:
reconsider domfc = domfc as finite set by A327;
set SL = Sgm domfc;
deffunc H₂( object ) -> set = vs . $1;
consider fvs being Function such that
A331: dom fvs = { k where k is Nat : ( 1 <= k & k <= n ) } and
A332: for x being object st x in { k where k is Nat : ( 1 <= k & k <= n ) } holds
fvs . x = H₂(x) from FUNCT_1:sch 3();
A333: n <= len vs by A4, A5, XXREAL_0:2;
{ k where k is Nat : ( 1 <= k & k <= n ) } c= Seg (len vs)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Nat : ( 1 <= k & k <= n ) } ; :: thesis:
then consider kk being Nat such that
A334: x = kk and
A335: 1 <= kk and
A336: kk <= n ;
kk <= len vs by A333, A336, XXREAL_0:2;
hence x in Seg (len vs) by A334, A335; :: thesis:

end;

then reconsider fvs = fvs as FinSubsequence by A331, FINSEQ_1:def 12;
fvs c= vs

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A337: p in fvs ; :: thesis:
then consider x, y being object such that
A338: [x,y] = p by RELAT_1:def 1;
A339: x in dom fvs by A337, A338, FUNCT_1:1;
then consider kk being Nat such that
A340: x = kk and
A341: 1 <= kk and
A342: kk <= n by A331;
kk <= len vs by A333, A342, XXREAL_0:2;
then A343: x in dom vs by A340, A341, FINSEQ_3:25;
y = fvs . x by A337, A338, FUNCT_1:1;
then y = vs . kk by A331, A332, A339, A340;
hence p in vs by A338, A340, A343, FUNCT_1:1; :: thesis:

end;

then reconsider fvs = fvs as Subset of vs ;
{ k where k is Nat : ( 1 <= k & k <= n ) } c= Seg (len vs)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Nat : ( 1 <= k & k <= n ) } ; :: thesis:
then consider k being Nat such that
A344: x = k and
A345: 1 <= k and
A346: k <= n ;
k <= len vs by A333, A346, XXREAL_0:2;
hence x in Seg (len vs) by A344, A345; :: thesis:

end;

then reconsider domfvs = { k where k is Nat : ( 1 <= k & k <= n ) } as finite set ;
take fvs ; :: thesis:
take c9 = c1; :: thesis:
take p1 = (1,n) -cut vs; :: thesis:
A347: (1,n) -cut vs is_vertex_seq_of c1 by A2, A12, A315, A311, Th42;
then A348: len ((1,n) -cut vs) = (len c1) + 1 ;
thus len c9 < len c by A10, A311, A317, XREAL_0:def 2; :: thesis:
thus p1 is_vertex_seq_of c9 by A2, A12, A315, A311, Th42; :: thesis:
len p1 = (len c1) + 1 by A347;
hence len p1 < len vs by A4, A5, A318, XXREAL_0:2; :: thesis:
thus vs . 1 = p1 . 1 by A3, A333, FINSEQ_6:138; :: thesis:
thus vs . (len vs) = p1 . (len p1) by A3, A4, A6, A308, FINSEQ_6:138; :: thesis:
A349: Sgm domfc = idseq n1 by FINSEQ_3:48;
then A350: dom (Sgm domfc) = Seg n1 ;

now :: thesis:

let p be object ; :: thesis:

hereby :: thesis:

assume A351: p in c1 ; :: thesis:
then consider x, y being object such that
A352: p = [x,y] by RELAT_1:def 1;
A353: y = c1 . x by A351, A352, FUNCT_1:1;
A354: x in dom c1 by A351, A352, FUNCT_1:1;
then reconsider k = x as Element of NAT ;
A355: k <= len c1 by A354, FINSEQ_3:25;
A356: 1 <= k by A354, FINSEQ_3:25;
then x in dom (Sgm domfc) by A317, A350, A355;
then A357: k = (Sgm domfc) . k by A349, FUNCT_1:18;
0 + 1 <= k by A354, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A358: i < n1 and
A359: k = i + 1 by A317, A355, FINSEQ_6:127;
A360: k in domfc by A317, A356, A355;
then A361: x in dom (fc * (Sgm domfc)) by A309, A350, A357, FUNCT_1:11;
then (fc * (Sgm domfc)) . x = fc . k by A357, FUNCT_1:12
.= c . (1 + i) by A309, A360, A359, GRFUNC_1:2
.= y by A11, A311, A316, A317, A353, A358, A359, Lm2 ;
hence p in fc * (Sgm domfc) by A352, A361, FUNCT_1:1; :: thesis:

end;

assume A362: p in fc * (Sgm domfc) ; :: thesis:
then consider x, y being object such that
A363: p = [x,y] by RELAT_1:def 1;
A364: y = (fc * (Sgm domfc)) . x by A362, A363, FUNCT_1:1;
A365: x in dom (fc * (Sgm domfc)) by A362, A363, FUNCT_1:1;
then A366: (fc * (Sgm domfc)) . x = fc . ((Sgm domfc) . x) by FUNCT_1:12;
A367: x in dom (Sgm domfc) by A365, FUNCT_1:11;
then consider k being Nat such that
A368: k = x and
A369: 1 <= k and
A370: k <= n1 by A350;
A371: k in dom fc by A309, A369, A370;
A372: k in dom c1 by A317, A369, A370, FINSEQ_3:25;
A373: k = (Sgm domfc) . k by A349, A367, A368, FUNCT_1:18;
0 + 1 <= k by A369;
then ex i being Nat st
( 0 <= i & i < n1 & k = i + 1 ) by A370, FINSEQ_6:127;
then c1 . k = c . k by A11, A311, A316, A317, Lm2
.= y by A364, A366, A368, A371, A373, GRFUNC_1:2 ;
hence p in c1 by A363, A368, A372, FUNCT_1:1; :: thesis:

end;

hence Seq fc = c9 by A309, TARSKI:2; :: thesis:
set SL = Sgm domfvs;
A374: Sgm domfvs = idseq n by FINSEQ_3:48;
then A375: dom (Sgm domfvs) = Seg n ;

now :: thesis:

let p be object ; :: thesis:

hereby :: thesis:

assume A376: p in (1,n) -cut vs ; :: thesis:
then consider x, y being object such that
A377: p = [x,y] by RELAT_1:def 1;
A378: y = ((1,n) -cut vs) . x by A376, A377, FUNCT_1:1;
A379: x in dom ((1,n) -cut vs) by A376, A377, FUNCT_1:1;
then reconsider k = x as Element of NAT ;
A380: k <= len ((1,n) -cut vs) by A379, FINSEQ_3:25;
A381: 1 <= k by A379, FINSEQ_3:25;
then x in dom (Sgm domfvs) by A348, A318, A375, A380;
then A382: k = (Sgm domfvs) . k by A374, FUNCT_1:18;
0 + 1 <= k by A379, FINSEQ_3:25;
then consider i being Nat such that
0 <= i and
A383: i < n and
A384: k = i + 1 by A348, A318, A380, FINSEQ_6:127;
A385: k in domfvs by A348, A318, A381, A380;
then A386: x in dom (fvs * (Sgm domfvs)) by A331, A375, A382, FUNCT_1:11;
then (fvs * (Sgm domfvs)) . x = fvs . k by A382, FUNCT_1:12
.= vs . (1 + i) by A331, A385, A384, GRFUNC_1:2
.= y by A3, A333, A348, A318, A378, A383, A384, FINSEQ_6:def 4 ;
hence p in fvs * (Sgm domfvs) by A377, A386, FUNCT_1:1; :: thesis:

end;

assume A387: p in fvs * (Sgm domfvs) ; :: thesis:
then consider x, y being object such that
A388: p = [x,y] by RELAT_1:def 1;
A389: y = (fvs * (Sgm domfvs)) . x by A387, A388, FUNCT_1:1;
A390: x in dom (fvs * (Sgm domfvs)) by A387, A388, FUNCT_1:1;
then A391: (fvs * (Sgm domfvs)) . x = fvs . ((Sgm domfvs) . x) by FUNCT_1:12;
A392: x in dom (Sgm domfvs) by A390, FUNCT_1:11;
then consider k being Nat such that
A393: k = x and
A394: 1 <= k and
A395: k <= n by A375;
A396: k in dom fvs by A331, A394, A395;
A397: k in dom ((1,n) -cut vs) by A348, A318, A394, A395, FINSEQ_3:25;
A398: k = (Sgm domfvs) . k by A374, A392, A393, FUNCT_1:18;
0 + 1 <= k by A394;
then ex i being Nat st
( 0 <= i & i < n & k = i + 1 ) by A395, FINSEQ_6:127;
then ((1,n) -cut vs) . k = vs . k by A3, A333, A348, A318, FINSEQ_6:def 4
.= y by A389, A391, A393, A396, A398, GRFUNC_1:2 ;
hence p in (1,n) -cut vs by A388, A393, A397, FUNCT_1:1; :: thesis:

end;

hence Seq fvs = p1 by A331, TARSKI:2; :: thesis:

end;