let G be Graph; 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; 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; ( 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
; 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; ( 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
; 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; verum