let G be Graph; :: thesis: for vs being FinSequence of the carrier of G
for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
for k being Nat st k in dom c holds
vs . k <> vs . (k + 1)

let vs be FinSequence of the carrier of G; :: thesis: for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
for k being Nat st k in dom c holds
vs . k <> vs . (k + 1)

let c be Chain of G; :: thesis: ( c alternates_vertices_in G & vs is_vertex_seq_of c implies for k being Nat st k in dom c holds
vs . k <> vs . (k + 1) )

assume that
A1: c alternates_vertices_in G and
A2: vs is_vertex_seq_of c ; :: thesis: for k being Nat st k in dom c holds
vs . k <> vs . (k + 1)

set TG = the Target of G;
set SG = the Source of G;
let k be Nat; :: thesis: ( k in dom c implies vs . k <> vs . (k + 1) )
set px = vs /. k;
set px1 = vs /. (k + 1);
assume A3: k in dom c ; :: thesis: vs . k <> vs . (k + 1)
then A4: k <= len c by FINSEQ_3:25;
A5: 1 <= k by ;
then c . k joins vs /. k,vs /. (k + 1) by A2, A4;
then A6: ( ( the Target of G . (c . k) = vs /. (k + 1) & the Source of G . (c . k) = vs /. k ) or ( the Target of G . (c . k) = vs /. k & the Source of G . (c . k) = vs /. (k + 1) ) ) ;
A7: len vs = (len c) + 1 by A2;
then k <= len vs by ;
then A8: vs /. k = vs . k by ;
1 <= k + 1 by NAT_1:12;
then vs /. (k + 1) = vs . (k + 1) by ;
hence vs . k <> vs . (k + 1) by A1, A3, A8, A6; :: thesis: verum