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

vs is TwoValued Alternating FinSequence

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

vs is TwoValued Alternating FinSequence

let c be Chain of G; :: thesis: ( c alternates_vertices_in G & vs is_vertex_seq_of c implies vs is TwoValued Alternating FinSequence )

assume that

A1: c alternates_vertices_in G and

A2: vs is_vertex_seq_of c ; :: thesis: vs is TwoValued Alternating FinSequence

A3: c <> {} by A1;

A4: len vs = (len c) + 1 by A2;

hence vs is TwoValued Alternating FinSequence by A5, FINSEQ_6:def 6, FINSEQ_6:def 7; :: thesis: verum

for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds

vs is TwoValued Alternating FinSequence

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

vs is TwoValued Alternating FinSequence

let c be Chain of G; :: thesis: ( c alternates_vertices_in G & vs is_vertex_seq_of c implies vs is TwoValued Alternating FinSequence )

assume that

A1: c alternates_vertices_in G and

A2: vs is_vertex_seq_of c ; :: thesis: vs is TwoValued Alternating FinSequence

A3: c <> {} by A1;

A4: len vs = (len c) + 1 by A2;

A5: now :: thesis: for k being Nat st 1 <= k & k + 1 <= len vs holds

vs . k <> vs . (k + 1)

card (rng vs) = 2
by A2, A3, Th31, A1;vs . k <> vs . (k + 1)

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len vs implies vs . k <> vs . (k + 1) )

assume that

A6: 1 <= k and

A7: k + 1 <= len vs ; :: thesis: vs . k <> vs . (k + 1)

k <= len c by A4, A7, XREAL_1:6;

hence vs . k <> vs . (k + 1) by A1, A2, Th35, A6, FINSEQ_3:25; :: thesis: verum

end;assume that

A6: 1 <= k and

A7: k + 1 <= len vs ; :: thesis: vs . k <> vs . (k + 1)

k <= len c by A4, A7, XREAL_1:6;

hence vs . k <> vs . (k + 1) by A1, A2, Th35, A6, FINSEQ_3:25; :: thesis: verum

hence vs is TwoValued Alternating FinSequence by A5, FINSEQ_6:def 6, FINSEQ_6:def 7; :: thesis: verum