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
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) ) )
per cases ( n <= len c or len c <= n ) ;
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) ) )

then A6: n + 1 <= len vs by ;
then A7: len vs1 = n + 1 by ;
A8: len c1 = n by ;
hence len vs1 = (len c1) + 1 by ; :: 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 ;
k + 1 <= (len c1) + 1 by ;
then k + 1 in Seg (n + 1) by ;
then A13: vs1 . (k + 1) = vs . (k + 1) by ;
A14: k <= len c by ;
then k <= len vs by ;
then A15: vs /. k = vs . k by ;
A16: k <= n + 1 by ;
then A17: vs1 /. k = vs1 . k by ;
k in Seg n by A8, A9, A10;
then A18: c1 . k = c . k by ;
k in Seg (n + 1) by ;
then A19: vs1 . k = vs . k by ;
vs /. (k + 1) = vs . (k + 1) by ;
hence c1 . k joins vs1 /. k,vs1 /. (k + 1) by A1, A9, A14, A18, A19, A13, A15, A17, A12; :: thesis: verum
end;
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) ) )

then len vs <= n + 1 by ;
then A21: vs1 = vs by ;
c1 = c by ;
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 ; :: thesis: verum
end;
end;
end;
hence vs1 is_vertex_seq_of c1 ; :: thesis: verum