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

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

end;

end;

hence vs1 is_vertex_seq_of c1 ; :: thesis: verum