let n be Nat; :: thesis: for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_vertex_seq_of c1

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

for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_vertex_seq_of c1

let vs, vs1 be FinSequence of the carrier of G; :: thesis: for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_vertex_seq_of c1

let c, c1 be Chain of G; :: thesis: ( vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) implies vs1 is_vertex_seq_of c1 )

assume A1: vs is_vertex_seq_of c ; :: thesis: ( not c1 = c | (Seg n) or not vs1 = vs | (Seg (n + 1)) or vs1 is_vertex_seq_of c1 )

then A2: len vs = (len c) + 1 ;

assume that

A3: c1 = c | (Seg n) and

A4: vs1 = vs | (Seg (n + 1)) ; :: thesis: vs1 is_vertex_seq_of c1

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_vertex_seq_of c1

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

for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_vertex_seq_of c1

let vs, vs1 be FinSequence of the carrier of G; :: thesis: for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_vertex_seq_of c1

let c, c1 be Chain of G; :: thesis: ( vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) implies vs1 is_vertex_seq_of c1 )

assume A1: vs is_vertex_seq_of c ; :: thesis: ( not c1 = c | (Seg n) or not vs1 = vs | (Seg (n + 1)) or vs1 is_vertex_seq_of c1 )

then A2: len vs = (len c) + 1 ;

assume that

A3: c1 = c | (Seg n) and

A4: vs1 = vs | (Seg (n + 1)) ; :: thesis: vs1 is_vertex_seq_of c1

now :: thesis: ( len vs1 = (len c1) + 1 & ( for k being Nat st 1 <= k & k <= len c1 holds

c1 . k joins vs1 /. k,vs1 /. (k + 1) ) )end;

hence
vs1 is_vertex_seq_of c1
; :: thesis: verumc1 . k joins vs1 /. k,vs1 /. (k + 1) ) )

per cases
( n <= len c or len c <= n )
;

end;

suppose A5:
n <= len c
; :: thesis: ( len vs1 = (len c1) + 1 & ( for k being Nat st 1 <= k & k <= len c1 holds

c1 . k joins vs1 /. k,vs1 /. (k + 1) ) )

c1 . k joins vs1 /. k,vs1 /. (k + 1) ) )

then A6:
n + 1 <= len vs
by A2, XREAL_1:6;

then A7: len vs1 = n + 1 by A4, FINSEQ_1:17;

A8: len c1 = n by A3, A5, FINSEQ_1:17;

hence len vs1 = (len c1) + 1 by A4, A6, FINSEQ_1:17; :: thesis: for k being Nat st 1 <= k & k <= len c1 holds

c1 . k joins vs1 /. k,vs1 /. (k + 1)

let k be Nat; :: thesis: ( 1 <= k & k <= len c1 implies c1 . k joins vs1 /. k,vs1 /. (k + 1) )

assume that

A9: 1 <= k and

A10: k <= len c1 ; :: thesis: c1 . k joins vs1 /. k,vs1 /. (k + 1)

A11: 1 <= k + 1 by NAT_1:12;

then A12: vs1 /. (k + 1) = vs1 . (k + 1) by A8, A7, A10, FINSEQ_4:15, XREAL_1:7;

k + 1 <= (len c1) + 1 by A10, XREAL_1:7;

then k + 1 in Seg (n + 1) by A8, A11;

then A13: vs1 . (k + 1) = vs . (k + 1) by A4, FUNCT_1:49;

A14: k <= len c by A5, A8, A10, XXREAL_0:2;

then k <= len vs by A2, NAT_1:12;

then A15: vs /. k = vs . k by A9, FINSEQ_4:15;

A16: k <= n + 1 by A8, A10, NAT_1:12;

then A17: vs1 /. k = vs1 . k by A7, A9, FINSEQ_4:15;

k in Seg n by A8, A9, A10;

then A18: c1 . k = c . k by A3, FUNCT_1:49;

k in Seg (n + 1) by A9, A16;

then A19: vs1 . k = vs . k by A4, FUNCT_1:49;

vs /. (k + 1) = vs . (k + 1) by A2, A14, A11, FINSEQ_4:15, XREAL_1:7;

hence c1 . k joins vs1 /. k,vs1 /. (k + 1) by A1, A9, A14, A18, A19, A13, A15, A17, A12; :: thesis: verum

end;then A7: len vs1 = n + 1 by A4, FINSEQ_1:17;

A8: len c1 = n by A3, A5, FINSEQ_1:17;

hence len vs1 = (len c1) + 1 by A4, A6, FINSEQ_1:17; :: thesis: for k being Nat st 1 <= k & k <= len c1 holds

c1 . k joins vs1 /. k,vs1 /. (k + 1)

let k be Nat; :: thesis: ( 1 <= k & k <= len c1 implies c1 . k joins vs1 /. k,vs1 /. (k + 1) )

assume that

A9: 1 <= k and

A10: k <= len c1 ; :: thesis: c1 . k joins vs1 /. k,vs1 /. (k + 1)

A11: 1 <= k + 1 by NAT_1:12;

then A12: vs1 /. (k + 1) = vs1 . (k + 1) by A8, A7, A10, FINSEQ_4:15, XREAL_1:7;

k + 1 <= (len c1) + 1 by A10, XREAL_1:7;

then k + 1 in Seg (n + 1) by A8, A11;

then A13: vs1 . (k + 1) = vs . (k + 1) by A4, FUNCT_1:49;

A14: k <= len c by A5, A8, A10, XXREAL_0:2;

then k <= len vs by A2, NAT_1:12;

then A15: vs /. k = vs . k by A9, FINSEQ_4:15;

A16: k <= n + 1 by A8, A10, NAT_1:12;

then A17: vs1 /. k = vs1 . k by A7, A9, FINSEQ_4:15;

k in Seg n by A8, A9, A10;

then A18: c1 . k = c . k by A3, FUNCT_1:49;

k in Seg (n + 1) by A9, A16;

then A19: vs1 . k = vs . k by A4, FUNCT_1:49;

vs /. (k + 1) = vs . (k + 1) by A2, A14, A11, FINSEQ_4:15, XREAL_1:7;

hence c1 . k joins vs1 /. k,vs1 /. (k + 1) by A1, A9, A14, A18, A19, A13, A15, A17, A12; :: thesis: verum

suppose A20:
len c <= n
; :: thesis: ( len vs1 = (len c1) + 1 & ( for k being Nat st 1 <= k & k <= len c1 holds

c1 . k joins vs1 /. k,vs1 /. (k + 1) ) )

c1 . k joins vs1 /. k,vs1 /. (k + 1) ) )

then
len vs <= n + 1
by A2, XREAL_1:6;

then A21: vs1 = vs by A4, FINSEQ_2:20;

c1 = c by A3, A20, FINSEQ_2:20;

hence ( len vs1 = (len c1) + 1 & ( for k being Nat st 1 <= k & k <= len c1 holds

c1 . k joins vs1 /. k,vs1 /. (k + 1) ) ) by A1, A21; :: thesis: verum

end;then A21: vs1 = vs by A4, FINSEQ_2:20;

c1 = c by A3, A20, FINSEQ_2:20;

hence ( len vs1 = (len c1) + 1 & ( for k being Nat st 1 <= k & k <= len c1 holds

c1 . k joins vs1 /. k,vs1 /. (k + 1) ) ) by A1, A21; :: thesis: verum