let G be Graph; :: thesis:
let vs be FinSequence of the carrier of G; :: thesis:
let c be Chain of G; :: thesis:
assume A1: vs is_vertex_seq_of c ; :: thesis:

hereby :: thesis:

assume A2: ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) ; :: thesis:

per cases by A2;

suppose A3: card the carrier of G = 1 ; :: thesis:

then reconsider tVG = the carrier of G as finite set ;
consider X being set such that
A4: tVG = {X} by A3, CARD_2:60;
let vs1 be FinSequence of the carrier of G; :: thesis:
assume A5: vs1 is_vertex_seq_of c ; :: thesis:
assume A6: vs1 <> vs ; :: thesis:
A7: ( len vs1 = (len c) + 1 & len vs = (len c) + 1 ) by A1, A5, Def7;
A8: ( Seg (len vs1) = dom vs1 & Seg (len vs) = dom vs ) by FINSEQ_1:def 3;
consider j being Nat such that
A9: ( j in dom vs & vs1 . j <> vs . j ) by A6, A7, FINSEQ_2:10;
A10: ( vs1 . j in rng vs1 & vs . j in rng vs ) by A7, A8, A9, FUNCT_1:def 5;
( rng vs1 c= {X} & rng vs c= {X} ) by A4, FINSEQ_1:def 4;
then ( vs . j = X & vs1 . j = X ) by A10, TARSKI:def 1;
hence contradiction by A9; :: thesis:

end;

suppose A11: ( c <> {} & not c alternates_vertices_in G ) ; :: thesis:

thus for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs :: thesis:

proof

let vs1 be FinSequence of the carrier of G; :: thesis:
assume A12: vs1 is_vertex_seq_of c ; :: thesis:
assume A13: vs1 <> vs ; :: thesis:
set SG = the Source of G;
set TG = the Target of G;
A14: ( len vs1 = (len c) + 1 & len vs = (len c) + 1 ) by A1, A12, Def7;
then A15: dom vs1 = dom vs by FINSEQ_3:31;
defpred S₁[ Nat] means ( $1 in dom vs1 & vs1 . $1 <> vs . $1 );
A16: ex i being Nat st S₁[i] by A13, A14, FINSEQ_2:10;
consider k being Nat such that
A17: S₁[k] and
A18: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A16);
A19: ( ( 0 + 1 = 1 & k = 0 ) or 0 + 1 <= k ) by NAT_1:13;

per cases by A19, XXREAL_0:1;

suppose k = 0 ; :: thesis:

hence contradiction by A17, FINSEQ_3:27; :: thesis:

end;

suppose A20: k = 1 ; :: thesis:

thus contradiction :: thesis:

proof

A21: ( 0 + 1 = 1 & ( len c = 0 or 0 < len c ) ) ;

per cases by A21, NAT_1:13;

suppose len c = 0 ; :: thesis:

hence contradiction by A11; :: thesis:

end;

suppose A22: 1 <= len c ; :: thesis:

then ( 1 <= k + 1 & k + 1 <= len vs1 ) by A14, A20, XREAL_1:8;
then A23: ( vs1 /. k = vs1 . k & vs1 /. (k + 1) = vs1 . (k + 1) & vs /. k = vs . k & vs /. (k + 1) = vs . (k + 1) ) by A14, A15, A17, FINSEQ_4:24, PARTFUN1:def 8;
A24: c . k joins vs1 /. k,vs1 /. (k + 1) by A12, A20, A22, Def7;
c . k joins vs /. k,vs /. (k + 1) by A1, A20, A22, Def7;
then A25: ( ( ( the Source of G . (c . 1) = vs1 /. 1 & the Target of G . (c . 1) = vs1 /. (k + 1) ) or ( the Source of G . (c . 1) = vs1 /. (k + 1) & the Target of G . (c . 1) = vs1 /. 1 ) ) & ( ( the Source of G . (c . 1) = vs /. 1 & the Target of G . (c . 1) = vs /. (k + 1) ) or ( the Source of G . (c . 1) = vs /. (k + 1) & the Target of G . (c . 1) = vs /. 1 ) ) ) by A20, A24, GRAPH_1:def 10;
defpred S₂[ Element of NAT ] means ( $1 in dom c implies ( vs1 /. $1 <> vs /. $1 & vs1 /. ($1 + 1) <> vs /. ($1 + 1) & ( ( the Target of G . (c . $1) = the Target of G . (c . 1) & the Source of G . (c . $1) = the Source of G . (c . 1) ) or ( the Target of G . (c . $1) = the Source of G . (c . 1) & the Source of G . (c . $1) = the Target of G . (c . 1) ) ) ) );
A26: S₂[ 0 ] by FINSEQ_3:27;

A27: now

let n be Element of NAT ; :: thesis:
assume A28: S₂[n] ; :: thesis:
thus S₂[n + 1] :: thesis:

proof

assume n + 1 in dom c ; :: thesis:
then A29: ( 1 <= n + 1 & n + 1 <= len c ) by FINSEQ_3:27;
thus ( vs1 /. (n + 1) <> vs /. (n + 1) & vs1 /. ((n + 1) + 1) <> vs /. ((n + 1) + 1) & ( ( the Target of G . (c . (n + 1)) = the Target of G . (c . 1) & the Source of G . (c . (n + 1)) = the Source of G . (c . 1) ) or ( the Target of G . (c . (n + 1)) = the Source of G . (c . 1) & the Source of G . (c . (n + 1)) = the Target of G . (c . 1) ) ) ) :: thesis:

proof

per cases ;

suppose A30: n = 0 ; :: thesis:

1 <= len c by A29, XXREAL_0:2;
then ( c . 1 joins vs1 /. 1,vs1 /. (1 + 1) & c . 1 joins vs /. 1,vs /. (1 + 1) ) by A1, A12, Def7;
then A31: ( ( ( the Source of G . (c . 1) = vs1 /. 1 & the Target of G . (c . 1) = vs1 /. (1 + 1) ) or ( the Source of G . (c . 1) = vs1 /. (1 + 1) & the Target of G . (c . 1) = vs1 /. 1 ) ) & ( ( the Source of G . (c . 1) = vs /. 1 & the Target of G . (c . 1) = vs /. (1 + 1) ) or ( the Source of G . (c . 1) = vs /. (1 + 1) & the Target of G . (c . 1) = vs /. 1 ) ) ) by GRAPH_1:def 10;
thus vs1 /. (n + 1) <> vs /. (n + 1) by A17, A20, A23, A30; :: thesis:
thus vs1 /. ((n + 1) + 1) <> vs /. ((n + 1) + 1) by A17, A20, A23, A30, A31; :: thesis:
thus ( ( the Target of G . (c . (n + 1)) = the Target of G . (c . 1) & the Source of G . (c . (n + 1)) = the Source of G . (c . 1) ) or ( the Target of G . (c . (n + 1)) = the Source of G . (c . 1) & the Source of G . (c . (n + 1)) = the Target of G . (c . 1) ) ) by A30; :: thesis:

end;

suppose 0 < n ; :: thesis:

then ( 0 + 1 <= n & n <= n + 1 ) by NAT_1:13;
then A32: ( 1 <= n & n <= len c ) by A29, XXREAL_0:2;
then A33: c . n joins vs1 /. n,vs1 /. (n + 1) by A12, Def7;
c . n joins vs /. n,vs /. (n + 1) by A1, A32, Def7;
then A34: ( ( ( the Source of G . (c . n) = vs1 /. n & the Target of G . (c . n) = vs1 /. (n + 1) ) or ( the Source of G . (c . n) = vs1 /. (n + 1) & the Target of G . (c . n) = vs1 /. n ) ) & ( ( the Source of G . (c . n) = vs /. n & the Target of G . (c . n) = vs /. (n + 1) ) or ( the Source of G . (c . n) = vs /. (n + 1) & the Target of G . (c . n) = vs /. n ) ) ) by A33, GRAPH_1:def 10;
A35: c . (n + 1) joins vs1 /. (n + 1),vs1 /. ((n + 1) + 1) by A12, A29, Def7;
c . (n + 1) joins vs /. (n + 1),vs /. ((n + 1) + 1) by A1, A29, Def7;
then A36: ( ( ( the Source of G . (c . (n + 1)) = vs1 /. (n + 1) & the Target of G . (c . (n + 1)) = vs1 /. ((n + 1) + 1) ) or ( the Source of G . (c . (n + 1)) = vs1 /. ((n + 1) + 1) & the Target of G . (c . (n + 1)) = vs1 /. (n + 1) ) ) & ( ( the Source of G . (c . (n + 1)) = vs /. (n + 1) & the Target of G . (c . (n + 1)) = vs /. ((n + 1) + 1) ) or ( the Source of G . (c . (n + 1)) = vs /. ((n + 1) + 1) & the Target of G . (c . (n + 1)) = vs /. (n + 1) ) ) ) by A35, GRAPH_1:def 10;
thus vs1 /. (n + 1) <> vs /. (n + 1) by A28, A32, FINSEQ_3:27; :: thesis:
thus vs1 /. ((n + 1) + 1) <> vs /. ((n + 1) + 1) by A28, A32, A36, FINSEQ_3:27; :: thesis:
thus ( ( the Target of G . (c . (n + 1)) = the Target of G . (c . 1) & the Source of G . (c . (n + 1)) = the Source of G . (c . 1) ) or ( the Target of G . (c . (n + 1)) = the Source of G . (c . 1) & the Source of G . (c . (n + 1)) = the Target of G . (c . 1) ) ) by A28, A32, A34, A36, FINSEQ_3:27; :: thesis:

end;

A37: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A26, A27);

A38: now

let n be Element of NAT ; :: thesis:
( not n in dom c or ( the Target of G . (c . n) = the Target of G . (c . 1) & the Source of G . (c . n) = the Source of G . (c . 1) ) or ( the Target of G . (c . n) = the Source of G . (c . 1) & the Source of G . (c . n) = the Target of G . (c . 1) ) ) by A37;
hence ( n in dom c implies the Source of G . (c . n) <> the Target of G . (c . n) ) by A17, A20, A23, A25; :: thesis:

end;

now

let x be set ; :: thesis:

hereby :: thesis:

assume x in G -VSet (rng c) ; :: thesis:
then consider v being Element of the carrier of G such that
A39: ( x = v & ex e being Element of the carrier' of G st
( e in rng c & ( v = the Source of G . e or v = the Target of G . e ) ) ) ;
consider e being set such that
A40: ( e in rng c & ( v = the Source of G . e or v = the Target of G . e ) ) by A39;
consider d being set such that
A41: ( d in dom c & e = c . d ) by A40, FUNCT_1:def 5;
reconsider d = d as Element of NAT by A41;
( ( the Target of G . (c . d) = the Target of G . (c . 1) & the Source of G . (c . d) = the Source of G . (c . 1) ) or ( the Target of G . (c . d) = the Source of G . (c . 1) & the Source of G . (c . d) = the Target of G . (c . 1) ) ) by A37, A41;
hence x in {(the Source of G . (c . 1)),(the Target of G . (c . 1))} by A39, A40, A41, TARSKI:def 2; :: thesis:

end;

assume A42: x in {(the Source of G . (c . 1)),(the Target of G . (c . 1))} ; :: thesis:
len c <> 0 by A11;
then 0 < len c ;
then 0 + 1 <= len c by NAT_1:13;
then A43: ( 1 in dom c & 1 in dom c ) by FINSEQ_3:27;
then A44: ( c . 1 in rng c & rng c c= the carrier' of G ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider e = c . 1 as Element of the carrier' of G ;
reconsider s = the Source of G . e as Element of the carrier of G by A44, FUNCT_2:7;
reconsider t = the Target of G . e as Element of the carrier of G by A44, FUNCT_2:7;
A45: e in rng c by A43, FUNCT_1:def 5;
( x = s or x = t ) by A42, TARSKI:def 2;
hence x in G -VSet (rng c) by A45; :: thesis:

end;

then G -VSet (rng c) = {(the Source of G . (c . 1)),(the Target of G . (c . 1))} by TARSKI:2;
then card (G -VSet (rng c)) = 2 by A17, A20, A23, A25, CARD_2:76;
hence contradiction by A11, A22, A38, Def8; :: thesis:

end;

suppose 1 < k ; :: thesis:

then 1 + 1 <= k by NAT_1:13;
then consider k1 being Element of NAT such that
A46: ( 1 <= k1 & k1 < k & k = k1 + 1 ) by Th1;
A47: k <= len vs1 by A17, FINSEQ_3:27;
then A48: k1 <= len c by A14, A46, XREAL_1:8;
A49: k1 <= len vs1 by A46, A47, XXREAL_0:2;
then A50: k1 in dom vs1 by A46, FINSEQ_3:27;
A51: ( vs1 /. k1 = vs1 . k1 & vs1 /. k = vs1 . k & vs /. k1 = vs . k1 & vs /. k = vs . k ) by A14, A15, A17, A46, A49, FINSEQ_4:24, PARTFUN1:def 8;
A52: c . k1 joins vs1 /. k1,vs1 /. (k1 + 1) by A12, A46, A48, Def7;
c . k1 joins vs /. k1,vs /. (k1 + 1) by A1, A46, A48, Def7;
then ( ( ( the Source of G . (c . k1) = vs1 /. k1 & the Target of G . (c . k1) = vs1 /. k ) or ( the Source of G . (c . k1) = vs1 /. k & the Target of G . (c . k1) = vs1 /. k1 ) ) & ( ( the Source of G . (c . k1) = vs /. k1 & the Target of G . (c . k1) = vs /. k ) or ( the Source of G . (c . k1) = vs /. k & the Target of G . (c . k1) = vs /. k1 ) ) ) by A46, A52, GRAPH_1:def 10;
hence contradiction by A17, A18, A46, A50, A51; :: thesis:

end;

assume A53: for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs ; :: thesis:
assume A54: card the carrier of G <> 1 ; :: thesis:
assume A55: ( c = {} or c alternates_vertices_in G ) ; :: thesis:
consider x, y being set such that
A56: ( x in the carrier of G & y in the carrier of G & x <> y ) by A54, Lm7;
reconsider x = x as Element of the carrier of G by A56;
reconsider y = y as Element of the carrier of G by A56;
thus contradiction :: thesis:

proof

per cases by A55;

suppose c = {} ; :: thesis:

then ( <*x*> = vs & <*y*> = vs ) by A53, Th35;
then ( vs . 1 = x & vs . 1 = y ) by FINSEQ_1:57;
hence contradiction by A56; :: thesis:

end;

suppose c alternates_vertices_in G ; :: thesis:

then consider vs1, vs2 being FinSequence of the carrier of G such that
A57: ( 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 ) ) ) by Th41;
( vs1 = vs & vs2 = vs ) by A53, A57;
hence contradiction by A57; :: thesis:

end;