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 Element of 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 Element of 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 Element of 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 Element of NAT st k in dom c holds
vs . k <> vs . (k + 1)
let k be Element of NAT ; :: thesis: ( k in dom c implies vs . k <> vs . (k + 1) )
assume A3: k in dom c ; :: thesis: vs . k <> vs . (k + 1)
then A4: ( 1 <= k & k <= len c ) by FINSEQ_3:27;
set SG = the Source of G;
set TG = the Target of G;
set px = vs /. k;
set px1 = vs /. (k + 1);
len vs = (len c) + 1 by A2, Def7;
then ( k <= len vs & 1 <= k + 1 & k + 1 <= len vs ) by A4, NAT_1:12, XREAL_1:9;
then A5: ( vs /. k = vs . k & vs /. (k + 1) = vs . (k + 1) ) by A4, FINSEQ_4:24;
c . k joins vs /. k,vs /. (k + 1) by A2, A4, Def7;
then ( ( 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) ) ) by GRAPH_1:def 10;
hence vs . k <> vs . (k + 1) by A1, A3, A5, Def8; :: thesis: verum