let G be Graph; :: thesis: for c being Chain of G st c alternates_vertices_in G holds

ex vs1, vs2 being FinSequence of the carrier of G st

( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

let c be Chain of G; :: thesis: ( c alternates_vertices_in G implies ex vs1, vs2 being FinSequence of the carrier of G st

( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) ) )

set X = the Source of G . (c . 1);

set Y = the Target of G . (c . 1);

consider p1 being FinSequence of the carrier of G such that

A1: p1 is_vertex_seq_of c by Th33;

assume A2: c alternates_vertices_in G ; :: thesis: ex vs1, vs2 being FinSequence of the carrier of G st

( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

then A3: 1 <= len c ;

then A4: 1 in dom c by FINSEQ_3:25;

A5: 1 + 1 = 2 ;

then A6: p1 . 1 <> p1 . 2 by A2, A1, A4, Th35;

A7: rng p1 = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A2, A1, Th36;

A8: len p1 = (len c) + 1 by A1;

then A9: len p1 > 1 by A3, NAT_1:13;

then consider p2 being TwoValued Alternating FinSequence such that

A10: rng p2 = {(p1 . 2),(p1 . 1)} and

A11: len p2 = len p1 and

A12: p2 . 1 = p1 . 2 by A6, FINSEQ_6:149;

A13: dom p1 = dom p2 by A11, FINSEQ_3:29;

1 + 1 <= len p1 by A9, NAT_1:13;

then 2 in dom p1 by FINSEQ_3:25;

then p1 . 2 in rng p1 by FUNCT_1:def 3;

then A14: ( p1 . 2 = the Source of G . (c . 1) or p1 . 2 = the Target of G . (c . 1) ) by A7, TARSKI:def 2;

1 in dom p1 by A9, FINSEQ_3:25;

then p1 . 1 in rng p1 by FUNCT_1:def 3;

then A15: ( p1 . 1 = the Source of G . (c . 1) or p1 . 1 = the Target of G . (c . 1) ) by A7, TARSKI:def 2;

then reconsider p2 = p2 as FinSequence of the carrier of G by A2, A1, A7, A4, A5, A10, A14, Th35, FINSEQ_1:def 4;

take p1 ; :: thesis: ex vs2 being FinSequence of the carrier of G st

( p1 <> vs2 & p1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = p1 or vs = vs2 ) ) )

take p2 ; :: thesis: ( p1 <> p2 & p1 is_vertex_seq_of c & p2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = p1 or vs = p2 ) ) )

thus p1 <> p2 by A2, A1, A4, A5, A12, Th35; :: thesis: ( p1 is_vertex_seq_of c & p2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = p1 or vs = p2 ) ) )

thus p1 is_vertex_seq_of c by A1; :: thesis: ( p2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = p1 or vs = p2 ) ) )

A16: p1 is TwoValued Alternating FinSequence by A2, A1, Th37;

( not vs is_vertex_seq_of c or vs = p1 or vs = p2 )

let p be FinSequence of the carrier of G; :: thesis: ( not p is_vertex_seq_of c or p = p1 or p = p2 )

assume A30: p is_vertex_seq_of c ; :: thesis: ( p = p1 or p = p2 )

then reconsider p9 = p as TwoValued Alternating FinSequence by A2, Th37;

A31: len p = (len c) + 1 by A30;

rng p = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A2, A30, Th36;

then ( p9 = p1 or p9 = p2 ) by A8, A7, A16, A6, A10, A11, A12, A15, A14, A31, FINSEQ_6:148;

hence ( p = p1 or p = p2 ) ; :: thesis: verum

ex vs1, vs2 being FinSequence of the carrier of G st

( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

let c be Chain of G; :: thesis: ( c alternates_vertices_in G implies ex vs1, vs2 being FinSequence of the carrier of G st

( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) ) )

set X = the Source of G . (c . 1);

set Y = the Target of G . (c . 1);

consider p1 being FinSequence of the carrier of G such that

A1: p1 is_vertex_seq_of c by Th33;

assume A2: c alternates_vertices_in G ; :: thesis: ex vs1, vs2 being FinSequence of the carrier of G st

( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

then A3: 1 <= len c ;

then A4: 1 in dom c by FINSEQ_3:25;

A5: 1 + 1 = 2 ;

then A6: p1 . 1 <> p1 . 2 by A2, A1, A4, Th35;

A7: rng p1 = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A2, A1, Th36;

A8: len p1 = (len c) + 1 by A1;

then A9: len p1 > 1 by A3, NAT_1:13;

then consider p2 being TwoValued Alternating FinSequence such that

A10: rng p2 = {(p1 . 2),(p1 . 1)} and

A11: len p2 = len p1 and

A12: p2 . 1 = p1 . 2 by A6, FINSEQ_6:149;

A13: dom p1 = dom p2 by A11, FINSEQ_3:29;

1 + 1 <= len p1 by A9, NAT_1:13;

then 2 in dom p1 by FINSEQ_3:25;

then p1 . 2 in rng p1 by FUNCT_1:def 3;

then A14: ( p1 . 2 = the Source of G . (c . 1) or p1 . 2 = the Target of G . (c . 1) ) by A7, TARSKI:def 2;

1 in dom p1 by A9, FINSEQ_3:25;

then p1 . 1 in rng p1 by FUNCT_1:def 3;

then A15: ( p1 . 1 = the Source of G . (c . 1) or p1 . 1 = the Target of G . (c . 1) ) by A7, TARSKI:def 2;

then reconsider p2 = p2 as FinSequence of the carrier of G by A2, A1, A7, A4, A5, A10, A14, Th35, FINSEQ_1:def 4;

take p1 ; :: thesis: ex vs2 being FinSequence of the carrier of G st

( p1 <> vs2 & p1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = p1 or vs = vs2 ) ) )

take p2 ; :: thesis: ( p1 <> p2 & p1 is_vertex_seq_of c & p2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = p1 or vs = p2 ) ) )

thus p1 <> p2 by A2, A1, A4, A5, A12, Th35; :: thesis: ( p1 is_vertex_seq_of c & p2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = p1 or vs = p2 ) ) )

thus p1 is_vertex_seq_of c by A1; :: thesis: ( p2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = p1 or vs = p2 ) ) )

A16: p1 is TwoValued Alternating FinSequence by A2, A1, Th37;

now :: thesis: ( len p2 = (len c) + 1 & ( for n being Nat st 1 <= n & n <= len c holds

c . n joins p2 /. n,p2 /. (n + 1) ) )

hence
p2 is_vertex_seq_of c
; :: thesis: for vs being FinSequence of the carrier of G holds c . n joins p2 /. n,p2 /. (n + 1) ) )

thus
len p2 = (len c) + 1
by A1, A11; :: thesis: for n being Nat st 1 <= n & n <= len c holds

c . n joins p2 /. n,p2 /. (n + 1)

let n be Nat; :: thesis: ( 1 <= n & n <= len c implies c . n joins p2 /. n,p2 /. (n + 1) )

assume that

A17: 1 <= n and

A18: n <= len c ; :: thesis: c . n joins p2 /. n,p2 /. (n + 1)

A19: n <= len p1 by A8, A18, NAT_1:12;

then A20: p2 /. n = p2 . n by A11, A17, FINSEQ_4:15;

A21: n in dom p1 by A17, A19, FINSEQ_3:25;

then p2 . n in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A2, A1, A4, A5, A10, A13, A15, A14, Th35, FUNCT_1:def 3;

then A22: ( p2 . n = the Source of G . (c . 1) or p2 . n = the Target of G . (c . 1) ) by TARSKI:def 2;

set x = p1 /. n;

set y = p1 /. (n + 1);

A23: c . n joins p1 /. n,p1 /. (n + 1) by A1, A17, A18;

A24: n + 1 <= len p1 by A8, A18, XREAL_1:6;

then A25: p2 /. (n + 1) = p2 . (n + 1) by A11, FINSEQ_4:15, NAT_1:12;

A26: 1 <= n + 1 by NAT_1:12;

then A27: n + 1 in dom p1 by A24, FINSEQ_3:25;

then p2 . (n + 1) in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A2, A1, A4, A5, A10, A13, A15, A14, Th35, FUNCT_1:def 3;

then A28: ( p2 . (n + 1) = the Source of G . (c . 1) or p2 . (n + 1) = the Target of G . (c . 1) ) by TARSKI:def 2;

p1 . n in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A7, A21, FUNCT_1:def 3;

then ( p1 . n = the Source of G . (c . 1) or p1 . n = the Target of G . (c . 1) ) by TARSKI:def 2;

then A29: p1 /. n = p2 . (n + 1) by A7, A16, A6, A10, A11, A12, A15, A14, A17, A19, A24, A22, A28, FINSEQ_6:def 7, FINSEQ_6:147, FINSEQ_4:15;

p1 . (n + 1) in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A7, A27, FUNCT_1:def 3;

then ( p1 . (n + 1) = the Source of G . (c . 1) or p1 . (n + 1) = the Target of G . (c . 1) ) by TARSKI:def 2;

then p1 /. (n + 1) = p2 . n by A7, A16, A6, A10, A11, A12, A15, A14, A17, A26, A24, A22, A28, FINSEQ_6:def 7, FINSEQ_6:147, FINSEQ_4:15;

hence c . n joins p2 /. n,p2 /. (n + 1) by A23, A29, A20, A25; :: thesis: verum

end;c . n joins p2 /. n,p2 /. (n + 1)

let n be Nat; :: thesis: ( 1 <= n & n <= len c implies c . n joins p2 /. n,p2 /. (n + 1) )

assume that

A17: 1 <= n and

A18: n <= len c ; :: thesis: c . n joins p2 /. n,p2 /. (n + 1)

A19: n <= len p1 by A8, A18, NAT_1:12;

then A20: p2 /. n = p2 . n by A11, A17, FINSEQ_4:15;

A21: n in dom p1 by A17, A19, FINSEQ_3:25;

then p2 . n in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A2, A1, A4, A5, A10, A13, A15, A14, Th35, FUNCT_1:def 3;

then A22: ( p2 . n = the Source of G . (c . 1) or p2 . n = the Target of G . (c . 1) ) by TARSKI:def 2;

set x = p1 /. n;

set y = p1 /. (n + 1);

A23: c . n joins p1 /. n,p1 /. (n + 1) by A1, A17, A18;

A24: n + 1 <= len p1 by A8, A18, XREAL_1:6;

then A25: p2 /. (n + 1) = p2 . (n + 1) by A11, FINSEQ_4:15, NAT_1:12;

A26: 1 <= n + 1 by NAT_1:12;

then A27: n + 1 in dom p1 by A24, FINSEQ_3:25;

then p2 . (n + 1) in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A2, A1, A4, A5, A10, A13, A15, A14, Th35, FUNCT_1:def 3;

then A28: ( p2 . (n + 1) = the Source of G . (c . 1) or p2 . (n + 1) = the Target of G . (c . 1) ) by TARSKI:def 2;

p1 . n in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A7, A21, FUNCT_1:def 3;

then ( p1 . n = the Source of G . (c . 1) or p1 . n = the Target of G . (c . 1) ) by TARSKI:def 2;

then A29: p1 /. n = p2 . (n + 1) by A7, A16, A6, A10, A11, A12, A15, A14, A17, A19, A24, A22, A28, FINSEQ_6:def 7, FINSEQ_6:147, FINSEQ_4:15;

p1 . (n + 1) in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A7, A27, FUNCT_1:def 3;

then ( p1 . (n + 1) = the Source of G . (c . 1) or p1 . (n + 1) = the Target of G . (c . 1) ) by TARSKI:def 2;

then p1 /. (n + 1) = p2 . n by A7, A16, A6, A10, A11, A12, A15, A14, A17, A26, A24, A22, A28, FINSEQ_6:def 7, FINSEQ_6:147, FINSEQ_4:15;

hence c . n joins p2 /. n,p2 /. (n + 1) by A23, A29, A20, A25; :: thesis: verum

( not vs is_vertex_seq_of c or vs = p1 or vs = p2 )

let p be FinSequence of the carrier of G; :: thesis: ( not p is_vertex_seq_of c or p = p1 or p = p2 )

assume A30: p is_vertex_seq_of c ; :: thesis: ( p = p1 or p = p2 )

then reconsider p9 = p as TwoValued Alternating FinSequence by A2, Th37;

A31: len p = (len c) + 1 by A30;

rng p = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A2, A30, Th36;

then ( p9 = p1 or p9 = p2 ) by A8, A7, A16, A6, A10, A11, A12, A15, A14, A31, FINSEQ_6:148;

hence ( p = p1 or p = p2 ) ; :: thesis: verum