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
set SG = the Source of G;
set TG = the Target of G;
A3: ( 1 <= len c & card (G -VSet (rng c)) = 2 & ( for n being Element of NAT st n in dom c holds
the Source of G . (c . n) <> the Target of G . (c . n) ) ) by A1, Def8;
c <> {} by A1, Def8, CARD_1:47;
then A4: card (rng vs) = 2 by A2, A3, Th34;
A5: ( len vs = (len c) + 1 & ( for n being Element of NAT st 1 <= n & n <= len c holds
c . n joins vs /. n,vs /. (n + 1) ) ) by A2, Def7;

now

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 A5, A7, XREAL_1:8;
then k in dom c by A6, FINSEQ_3:27;
hence vs . k <> vs . (k + 1) by A1, A2, Th38; :: thesis: verum

end;

hence vs is TwoValued Alternating FinSequence by A4, Def3, Def4; :: thesis: verum