let G be Graph; :: thesis: for vs being FinSequence of the carrier of G

for c being Chain of G st c is not simple Chain of G & vs is_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

let vs be FinSequence of the carrier of G; :: thesis: for c being Chain of G st c is not simple Chain of G & vs is_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

let c be Chain of G; :: thesis: ( c is not simple Chain of G & vs is_vertex_seq_of c implies ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) )

assume that

A1: c is not simple Chain of G and

A2: vs is_vertex_seq_of c ; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

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 ;

for c being Chain of G st c is not simple Chain of G & vs is_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

let vs be FinSequence of the carrier of G; :: thesis: for c being Chain of G st c is not simple Chain of G & vs is_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

let c be Chain of G; :: thesis: ( c is not simple Chain of G & vs is_vertex_seq_of c implies ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) )

assume that

A1: c is not simple Chain of G and

A2: vs is_vertex_seq_of c ; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

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
( ( n <> 1 & m <> len vs ) or ( n = 1 & m <> len vs ) or ( n <> 1 & m = len vs ) )
by A7;

end;

suppose A13:
( n <> 1 & m <> len vs )
; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

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_{1}( 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_{1}(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)

A25: fc c= c

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: ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

A34: pp is_vertex_seq_of c1 by A2, A12, A33, A21, Th42;

then A35: len pp = (len c1) + 1 ;

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

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

set DR = { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ;

A87: 1 <= m + 1 by NAT_1:12;

deffunc H_{2}( 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_{2}(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)

fvs c= 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: ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

take c9 ; :: thesis: ex vs1 being FinSequence of the carrier of G st

( len c9 < len c & vs1 is_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 )

take p1 = pp ^' p2; :: thesis: ( len c9 < len c & p1 is_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

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: ( p1 is_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

A108: Sgm DL = idseq n1 by FINSEQ_3:48;

then A109: dom (Sgm DL) = Seg n1 ;

thus p1 is_vertex_seq_of c9 by A6, A34, A53, A103, A104, Th44; :: thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

then len p1 = (len c9) + 1 ;

hence len p1 < len vs by A9, A107, XREAL_1:6; :: thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

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: ( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

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: ( Seq fc = c9 & Seq fvs = p1 )

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: Seq fvs = p1

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

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 ;

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;

(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: verum

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

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

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

then reconsider fc = fc as FinSubsequence by A19, FINSEQ_1:def 12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } or x in Seg (len c) )

assume x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; :: thesis: x in Seg (len c)

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: verum

end;assume x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; :: thesis: x in Seg (len c)

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: verum

A25: fc c= c

proof

1 < n
by A3, A13, XXREAL_0:1;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in fc or p in c )

assume A26: p in fc ; :: thesis: p in c

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: verum

end;assume A26: p in fc ; :: thesis: p in c

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: verum

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: ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

A34: pp is_vertex_seq_of c1 by A2, A12, A33, A21, Th42;

then A35: len pp = (len c1) + 1 ;

now :: thesis: for x being object holds

( ( x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } implies x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ) )

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;( ( x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } implies x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ) )

let x be object ; :: thesis: ( ( x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } implies b_{1} in { b_{2} where k is Nat : ( ( 1 <= b_{2} & b_{2} <= n1 ) or ( m <= b_{2} & b_{2} <= len c ) ) } ) )

_{1} in { b_{2} where k is Nat : ( ( 1 <= b_{2} & b_{2} <= n1 ) or ( m <= b_{2} & b_{2} <= len c ) ) }

end;hereby :: thesis: ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } implies b_{1} in { b_{2} where k is Nat : ( ( 1 <= b_{2} & b_{2} <= n1 ) or ( m <= b_{2} & b_{2} <= len c ) ) } )

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

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: verum

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

per cases
( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } or x in { kk where kk is Nat : ( m <= kk & kk <= len c ) } )
by A36, XBOOLE_0:def 3;

end;

suppose
x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) }
; :: thesis: b_{1} in { b_{2} where k is Nat : ( ( 1 <= b_{2} & b_{2} <= n1 ) or ( m <= b_{2} & b_{2} <= len c ) ) }

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: verum

end;( 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: verum

suppose
x in { kk where kk is Nat : ( m <= kk & kk <= len c ) }
; :: thesis: b_{1} in { b_{2} where k is Nat : ( ( 1 <= b_{2} & b_{2} <= n1 ) or ( m <= b_{2} & b_{2} <= len c ) ) }

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: verum

end;( 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: verum

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

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

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: verum

end;

then reconsider DR = { kk where kk is Nat : ( m <= kk & kk <= len c ) } as finite set ;hereby :: according to TARSKI:def 3 :: thesis: { kk where kk is Nat : ( m <= kk & kk <= len c ) } c= Seg (len c)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { kk where kk is Nat : ( m <= kk & kk <= len c ) } or x in Seg (len c) )let x be object ; :: thesis: ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } implies x in Seg (len c) )

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

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: verum

end;assume x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } ; :: thesis: x in Seg (len c)

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: verum

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

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: verum

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: for p being object holds

( ( p in c2 implies p in fc * (Sgm DR) ) & ( p in fc * (Sgm DR) implies p in c2 ) )

then A82:
c2 = fc * (Sgm DR)
by TARSKI:2;( ( p in c2 implies p in fc * (Sgm DR) ) & ( p in fc * (Sgm DR) implies p in c2 ) )

let p be object ; :: thesis: ( ( p in c2 implies p in fc * (Sgm DR) ) & ( p in fc * (Sgm DR) implies p in c2 ) )

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: verum

end;hereby :: thesis: ( p in fc * (Sgm DR) implies p in c2 )

assume A71:
p in fc * (Sgm DR)
; :: thesis: p in c2assume A60:
p in c2
; :: thesis: p in fc * (Sgm DR)

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: verum

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

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: verum

now :: thesis: for i, j being Nat st i in DL & j in DR holds

i < j

then A86:
Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR)
by A38, FINSEQ_3:42;i < j

let i, j be Nat; :: thesis: ( i in DL & j in DR implies i < j )

assume i in DL ; :: thesis: ( j in DR implies i < j )

then consider k being Nat such that

A83: k = i and

1 <= k and

A84: k <= n1 ;

assume j in DR ; :: thesis: i < j

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: verum

end;assume i in DL ; :: thesis: ( j in DR implies i < j )

then consider k being Nat such that

A83: k = i and

1 <= k and

A84: k <= n1 ;

assume j in DR ; :: thesis: i < j

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: verum

set DR = { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ;

A87: 1 <= m + 1 by NAT_1:12;

deffunc H

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

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

then reconsider fvs = fvs as FinSubsequence by A88, FINSEQ_1:def 12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } or x in Seg (len vs) )

assume x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; :: thesis: x in Seg (len vs)

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: verum

end;assume x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; :: thesis: x in Seg (len vs)

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: verum

fvs c= vs

proof

then reconsider fvs = fvs as Subset of vs ;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in fvs or p in vs )

assume A94: p in fvs ; :: thesis: p in vs

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: verum

end;assume A94: p in fvs ; :: thesis: p in vs

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: verum

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: ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

take c9 ; :: thesis: ex vs1 being FinSequence of the carrier of G st

( len c9 < len c & vs1 is_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 )

take p1 = pp ^' p2; :: thesis: ( len c9 < len c & p1 is_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

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: ( p1 is_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

A108: Sgm DL = idseq n1 by FINSEQ_3:48;

then A109: dom (Sgm DL) = Seg n1 ;

now :: thesis: for p being object holds

( ( p in c1 implies p in fc * (Sgm DL) ) & ( p in fc * (Sgm DL) implies p in c1 ) )

then A134:
c1 = fc * (Sgm DL)
by TARSKI:2;( ( p in c1 implies p in fc * (Sgm DL) ) & ( p in fc * (Sgm DL) implies p in c1 ) )

let p be object ; :: thesis: ( ( p in c1 implies p in fc * (Sgm DL) ) & ( p in fc * (Sgm DL) implies p in c1 ) )

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: verum

end;hereby :: thesis: ( p in fc * (Sgm DL) implies p in c1 )

assume A122:
p in fc * (Sgm DL)
; :: thesis: p in c1assume A110:
p in c1
; :: thesis: p in fc * (Sgm DL)

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: verum

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

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: verum

thus p1 is_vertex_seq_of c9 by A6, A34, A53, A103, A104, Th44; :: thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

then len p1 = (len c9) + 1 ;

hence len p1 < len vs by A9, A107, XREAL_1:6; :: thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

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: ( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

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: ( Seq fc = c9 & Seq fvs = p1 )

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: Seq fvs = p1

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

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

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: verum

end;

hereby :: according to TARSKI:def 3 :: thesis: { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } c= Seg (len vs)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } or x in Seg (len vs) )let x be object ; :: thesis: ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } implies x in Seg (len vs) )

assume x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } ; :: thesis: x in Seg (len vs)

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: verum

end;assume x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } ; :: thesis: x in Seg (len vs)

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: verum

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

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: verum

now :: thesis: for x being object holds

( ( x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } implies x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ) )

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;( ( x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } implies x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ) )

let x be object ; :: thesis: ( ( x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } implies b_{1} in { b_{2} where k is Nat : ( ( 1 <= b_{2} & b_{2} <= n ) or ( m + 1 <= b_{2} & b_{2} <= len vs ) ) } ) )

_{1} in { b_{2} where k is Nat : ( ( 1 <= b_{2} & b_{2} <= n ) or ( m + 1 <= b_{2} & b_{2} <= len vs ) ) }

end;hereby :: thesis: ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } implies b_{1} in { b_{2} where k is Nat : ( ( 1 <= b_{2} & b_{2} <= n ) or ( m + 1 <= b_{2} & b_{2} <= len vs ) ) } )

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: bassume
x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) }
; :: thesis: x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) }

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: verum

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

per cases
( 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 ) } )
by A143, XBOOLE_0:def 3;

end;

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

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: verum

end;( 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: verum

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

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: verum

end;( 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: verum

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: for p being object holds

( ( p in pp implies p in fvs * (Sgm DL) ) & ( p in fvs * (Sgm DL) implies p in pp ) )

then A175:
pp = fvs * (Sgm DL)
by TARSKI:2;( ( p in pp implies p in fvs * (Sgm DL) ) & ( p in fvs * (Sgm DL) implies p in pp ) )

let p be object ; :: thesis: ( ( p in pp implies p in fvs * (Sgm DL) ) & ( p in fvs * (Sgm DL) implies p in pp ) )

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: verum

end;hereby :: thesis: ( p in fvs * (Sgm DL) implies p in pp )

assume A163:
p in fvs * (Sgm DL)
; :: thesis: p in ppassume A151:
p in pp
; :: thesis: p in fvs * (Sgm DL)

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: verum

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

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: verum

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: for p being object holds

( ( p in ((m + 1),((len c) + 1)) -cut vs implies p in fvs * (Sgm DR) ) & ( p in fvs * (Sgm DR) implies p in ((m + 1),((len c) + 1)) -cut vs ) )

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

let p be object ; :: thesis: ( ( p in ((m + 1),((len c) + 1)) -cut vs implies p in fvs * (Sgm DR) ) & ( p in fvs * (Sgm DR) implies p in ((m + 1),((len c) + 1)) -cut vs ) )

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: verum

end;hereby :: thesis: ( p in fvs * (Sgm DR) implies p in ((m + 1),((len c) + 1)) -cut vs )

assume A191:
p in fvs * (Sgm DR)
; :: thesis: p in ((m + 1),((len c) + 1)) -cut vsassume A180:
p in ((m + 1),((len c) + 1)) -cut vs
; :: thesis: p in fvs * (Sgm DR)

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: verum

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

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: verum

now :: thesis: for i, j being Nat st i in DL & j in DR holds

i < j

then A208:
Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR)
by A136, FINSEQ_3:42;i < j

let i, j be Nat; :: thesis: ( i in DL & j in DR implies i < j )

assume i in DL ; :: thesis: ( j in DR implies i < j )

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: i < j

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: verum

end;assume i in DL ; :: thesis: ( j in DR implies i < j )

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: i < j

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: verum

(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: verum

suppose A210:
( n = 1 & m <> len vs )
; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

set domfvs = { k where k is Nat : ( m <= k & k <= len vs ) } ;

deffunc H_{1}( 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_{1}(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)

fc c= c

take fc ; :: thesis: ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

deffunc H_{2}( 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_{2}(x)
from FUNCT_1:sch 3();

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

A231: fvs c= vs

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: ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

take c1 = c2; :: thesis: ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

take p1 = (m,((len c) + 1)) -cut vs; :: thesis: ( len c1 < len c & p1 is_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

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: ( p1 is_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

1 <= m by A3, A4, XXREAL_0:2;

hence p1 is_vertex_seq_of c1 by A2, A241, Th42; :: thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

(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: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

thus vs . 1 = p1 . 1 by A4, A5, A6, A9, A210, FINSEQ_6:138; :: thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

thus vs . (len vs) = p1 . (len p1) by A4, A5, A9, A210, FINSEQ_6:138; :: thesis: ( Seq fc = c1 & Seq fvs = p1 )

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

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;

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

end;deffunc H

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

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

then reconsider fc = fc as FinSubsequence by A211, FINSEQ_1:def 12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : ( m <= k & k <= len c ) } or x in Seg (len c) )

assume x in { k where k is Nat : ( m <= k & k <= len c ) } ; :: thesis: x in Seg (len c)

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: verum

end;assume x in { k where k is Nat : ( m <= k & k <= len c ) } ; :: thesis: x in Seg (len c)

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: verum

fc c= c

proof

then reconsider fc = fc as Subset of c ;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in fc or p in c )

assume A219: p in fc ; :: thesis: p in c

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: verum

end;assume A219: p in fc ; :: thesis: p in c

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: verum

take fc ; :: thesis: ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

deffunc H

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

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

proof

then reconsider fvs = fvs as FinSubsequence by A226, FINSEQ_1:def 12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : ( m <= k & k <= len vs ) } or x in Seg (len vs) )

assume x in { k where k is Nat : ( m <= k & k <= len vs ) } ; :: thesis: x in Seg (len vs)

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: verum

end;assume x in { k where k is Nat : ( m <= k & k <= len vs ) } ; :: thesis: x in Seg (len vs)

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: verum

A231: fvs c= vs

proof

A239:
m < len vs
by A5, A210, XXREAL_0:1;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in fvs or p in vs )

assume A232: p in fvs ; :: thesis: p in vs

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: verum

end;assume A232: p in fvs ; :: thesis: p in vs

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: verum

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: ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

take c1 = c2; :: thesis: ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

take p1 = (m,((len c) + 1)) -cut vs; :: thesis: ( len c1 < len c & p1 is_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

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: ( p1 is_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

1 <= m by A3, A4, XXREAL_0:2;

hence p1 is_vertex_seq_of c1 by A2, A241, Th42; :: thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

(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: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

thus vs . 1 = p1 . 1 by A4, A5, A6, A9, A210, FINSEQ_6:138; :: thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )

thus vs . (len vs) = p1 . (len p1) by A4, A5, A9, A210, FINSEQ_6:138; :: thesis: ( Seq fc = c1 & Seq fvs = p1 )

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

proof

A248:
{ k where k is Nat : ( m <= k & k <= len c ) } c= Seg (len c)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : ( m <= k & k <= len vs ) } or x in Seg (len vs) )

assume x in { k where k is Nat : ( m <= k & k <= len vs ) } ; :: thesis: x in Seg (len vs)

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: verum

end;assume x in { k where k is Nat : ( m <= k & k <= len vs ) } ; :: thesis: x in Seg (len vs)

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: verum

proof

then reconsider domfc = { k where k is Nat : ( m <= k & k <= len c ) } as finite set ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : ( m <= k & k <= len c ) } or x in Seg (len c) )

assume x in { k where k is Nat : ( m <= k & k <= len c ) } ; :: thesis: x in Seg (len c)

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: verum

end;assume x in { k where k is Nat : ( m <= k & k <= len c ) } ; :: thesis: x in Seg (len c)

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: verum

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: for p being object holds

( ( p in c2 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c2 ) )

hence
Seq fc = c1
by A211, TARSKI:2; :: thesis: Seq fvs = p1( ( p in c2 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c2 ) )

let p be object ; :: thesis: ( ( p in c2 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c2 ) )

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: verum

end;hereby :: thesis: ( p in fc * (Sgm domfc) implies p in c2 )

assume A270:
p in fc * (Sgm domfc)
; :: thesis: p in c2assume A259:
p in c2
; :: thesis: p in fc * (Sgm domfc)

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: verum

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

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: verum

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: for p being object holds

( ( p in (m,((len c) + 1)) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (m,((len c) + 1)) -cut vs ) )

hence
Seq fvs = p1
by A226, TARSKI:2; :: thesis: verum( ( p in (m,((len c) + 1)) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (m,((len c) + 1)) -cut vs ) )

let p be object ; :: thesis: ( ( p in (m,((len c) + 1)) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (m,((len c) + 1)) -cut vs ) )

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: verum

end;hereby :: thesis: ( p in fvs * (Sgm domfvs) implies p in (m,((len c) + 1)) -cut vs )

assume A297:
p in fvs * (Sgm domfvs)
; :: thesis: p in (m,((len c) + 1)) -cut vsassume A286:
p in (m,((len c) + 1)) -cut vs
; :: thesis: p in fvs * (Sgm domfvs)

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: verum

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

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: verum

suppose A308:
( n <> 1 & m = len vs )
; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

set domfvs = { k where k is Nat : ( 1 <= k & k <= n ) } ;

set pp = (1,n) -cut vs;

deffunc H_{1}( 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_{1}(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)

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

take fc ; :: thesis: ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

reconsider domfc = domfc as finite set by A327;

set SL = Sgm domfc;

deffunc H_{2}( 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_{2}(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)

fvs c= vs

{ k where k is Nat : ( 1 <= k & k <= n ) } c= Seg (len vs)

take fvs ; :: thesis: ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

take c9 = c1; :: thesis: ex vs1 being FinSequence of the carrier of G st

( len c9 < len c & vs1 is_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 )

take p1 = (1,n) -cut vs; :: thesis: ( len c9 < len c & p1 is_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

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: ( p1 is_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

thus p1 is_vertex_seq_of c9 by A2, A12, A315, A311, Th42; :: thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

len p1 = (len c1) + 1 by A347;

hence len p1 < len vs by A4, A5, A318, XXREAL_0:2; :: thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

thus vs . 1 = p1 . 1 by A3, A333, FINSEQ_6:138; :: thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

thus vs . (len vs) = p1 . (len p1) by A3, A4, A6, A308, FINSEQ_6:138; :: thesis: ( Seq fc = c9 & Seq fvs = p1 )

A349: Sgm domfc = idseq n1 by FINSEQ_3:48;

then A350: dom (Sgm domfc) = Seg n1 ;

set SL = Sgm domfvs;

A374: Sgm domfvs = idseq n by FINSEQ_3:48;

then A375: dom (Sgm domfvs) = Seg n ;

end;set pp = (1,n) -cut vs;

deffunc H

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

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

then reconsider fc = fc as FinSubsequence by A309, FINSEQ_1:def 12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in domfc or x in Seg (len c) )

assume x in domfc ; :: thesis: x in Seg (len c)

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: verum

end;assume x in domfc ; :: thesis: x in Seg (len c)

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: verum

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

A327:
domfc c= Seg (len c)
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in fc or p in c )

assume A320: p in fc ; :: thesis: p in c

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: verum

end;assume A320: p in fc ; :: thesis: p in c

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: verum

proof

reconsider fc = fc as Subset of c by A319;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in domfc or x in Seg (len c) )

assume x in domfc ; :: thesis: x in Seg (len c)

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: verum

end;assume x in domfc ; :: thesis: x in Seg (len c)

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: verum

take fc ; :: thesis: ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

reconsider domfc = domfc as finite set by A327;

set SL = Sgm domfc;

deffunc H

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

A333: n <= len vs by A4, A5, XXREAL_0:2;

{ k where k is Nat : ( 1 <= k & k <= n ) } c= Seg (len vs)

proof

then reconsider fvs = fvs as FinSubsequence by A331, FINSEQ_1:def 12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : ( 1 <= k & k <= n ) } or x in Seg (len vs) )

assume x in { k where k is Nat : ( 1 <= k & k <= n ) } ; :: thesis: x in Seg (len vs)

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: verum

end;assume x in { k where k is Nat : ( 1 <= k & k <= n ) } ; :: thesis: x in Seg (len vs)

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: verum

fvs c= vs

proof

then reconsider fvs = fvs as Subset of vs ;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in fvs or p in vs )

assume A337: p in fvs ; :: thesis: p in vs

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: verum

end;assume A337: p in fvs ; :: thesis: p in vs

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: verum

{ k where k is Nat : ( 1 <= k & k <= n ) } c= Seg (len vs)

proof

then reconsider domfvs = { k where k is Nat : ( 1 <= k & k <= n ) } as finite set ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : ( 1 <= k & k <= n ) } or x in Seg (len vs) )

assume x in { k where k is Nat : ( 1 <= k & k <= n ) } ; :: thesis: x in Seg (len vs)

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: verum

end;assume x in { k where k is Nat : ( 1 <= k & k <= n ) } ; :: thesis: x in Seg (len vs)

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: verum

take fvs ; :: thesis: ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

take c9 = c1; :: thesis: ex vs1 being FinSequence of the carrier of G st

( len c9 < len c & vs1 is_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 )

take p1 = (1,n) -cut vs; :: thesis: ( len c9 < len c & p1 is_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

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: ( p1 is_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

thus p1 is_vertex_seq_of c9 by A2, A12, A315, A311, Th42; :: thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

len p1 = (len c1) + 1 by A347;

hence len p1 < len vs by A4, A5, A318, XXREAL_0:2; :: thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

thus vs . 1 = p1 . 1 by A3, A333, FINSEQ_6:138; :: thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )

thus vs . (len vs) = p1 . (len p1) by A3, A4, A6, A308, FINSEQ_6:138; :: thesis: ( Seq fc = c9 & Seq fvs = p1 )

A349: Sgm domfc = idseq n1 by FINSEQ_3:48;

then A350: dom (Sgm domfc) = Seg n1 ;

now :: thesis: for p being object holds

( ( p in c1 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c1 ) )

hence
Seq fc = c9
by A309, TARSKI:2; :: thesis: Seq fvs = p1( ( p in c1 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c1 ) )

let p be object ; :: thesis: ( ( p in c1 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c1 ) )

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: verum

end;hereby :: thesis: ( p in fc * (Sgm domfc) implies p in c1 )

assume A362:
p in fc * (Sgm domfc)
; :: thesis: p in c1assume A351:
p in c1
; :: thesis: p in fc * (Sgm domfc)

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: verum

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

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: verum

set SL = Sgm domfvs;

A374: Sgm domfvs = idseq n by FINSEQ_3:48;

then A375: dom (Sgm domfvs) = Seg n ;

now :: thesis: for p being object holds

( ( p in (1,n) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs ) )

hence
Seq fvs = p1
by A331, TARSKI:2; :: thesis: verum( ( p in (1,n) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs ) )

let p be object ; :: thesis: ( ( p in (1,n) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs ) )

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: verum

end;hereby :: thesis: ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs )

assume A387:
p in fvs * (Sgm domfvs)
; :: thesis: p in (1,n) -cut vsassume A376:
p in (1,n) -cut vs
; :: thesis: p in fvs * (Sgm domfvs)

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: verum

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

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: verum