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 A3, FINSEQ_3:25;
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 A4, NAT_1:12;
then A8: vs /. k = vs . k by A5, FINSEQ_4:15;
1 <= k + 1 by NAT_1:12;
then vs /. (k + 1) = vs . (k + 1) by A4, A7, FINSEQ_4:15, XREAL_1:7;
hence vs . k <> vs . (k + 1) by A1, A3, A8, A6; :: thesis: verum