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

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