let G be Graph; :: thesis: for vs being FinSequence of the carrier of G
for c being Chain of G st vs is_vertex_seq_of c holds
( ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) iff for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs )

let vs be FinSequence of the carrier of G; :: thesis: for c being Chain of G st vs is_vertex_seq_of c holds
( ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) iff for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs )

let c be Chain of G; :: thesis: ( vs is_vertex_seq_of c implies ( ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) iff for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs ) )

assume A1: vs is_vertex_seq_of c ; :: thesis: ( ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) iff for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs )

hereby :: thesis: ( ex vs1 being FinSequence of the carrier of G st
( vs1 is_vertex_seq_of c & not vs1 = vs ) or card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) )
assume A2: ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) ; :: thesis: for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
not vs1 <> vs

per cases ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) by A2;
suppose A3: card the carrier of G = 1 ; :: thesis: for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
not vs1 <> vs

then reconsider tVG = the carrier of G as finite set ;
consider X being object such that
A4: tVG = {X} by ;
A5: rng vs c= {X} by ;
A6: len vs = (len c) + 1 by A1;
let vs1 be FinSequence of the carrier of G; :: thesis: ( vs1 is_vertex_seq_of c implies not vs1 <> vs )
A7: Seg (len vs) = dom vs by FINSEQ_1:def 3;
assume vs1 is_vertex_seq_of c ; :: thesis: not vs1 <> vs
then A8: len vs1 = (len c) + 1 ;
assume vs1 <> vs ; :: thesis: contradiction
then consider j being Nat such that
A9: j in dom vs and
A10: vs1 . j <> vs . j by ;
vs . j in rng vs by ;
then A11: vs . j = X by ;
A12: rng vs1 c= {X} by ;
Seg (len vs1) = dom vs1 by FINSEQ_1:def 3;
then vs1 . j in rng vs1 by ;
hence contradiction by A10, A12, A11, TARSKI:def 1; :: thesis: verum
end;
suppose A13: ( c <> {} & not c alternates_vertices_in G ) ; :: thesis: for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs

thus for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs :: thesis: verum
proof
set TG = the Target of G;
set SG = the Source of G;
let vs1 be FinSequence of the carrier of G; :: thesis: ( vs1 is_vertex_seq_of c implies vs1 = vs )
defpred S1[ Nat] means ( \$1 in dom vs1 & vs1 . \$1 <> vs . \$1 );
assume A14: vs1 is_vertex_seq_of c ; :: thesis: vs1 = vs
then A15: len vs1 = (len c) + 1 ;
A16: len vs = (len c) + 1 by A1;
then A17: dom vs1 = dom vs by ;
assume vs1 <> vs ; :: thesis: contradiction
then A18: ex i being Nat st S1[i] by ;
consider k being Nat such that
A19: S1[k] and
A20: for n being Nat st S1[n] holds
k <= n from A21: ( ( 0 + 1 = 1 & k = 0 ) or 0 + 1 <= k ) by NAT_1:13;
per cases ( k = 0 or k = 1 or 1 < k ) by ;
suppose A22: k = 1 ; :: thesis: contradiction
thus contradiction :: thesis: verum
proof
A23: 0 + 1 = 1 ;
per cases ( len c = 0 or 1 <= len c ) by ;
suppose A24: 1 <= len c ; :: thesis: contradiction
defpred S2[ 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) ) ) ) );
A25: vs /. k = vs . k by ;
A26: vs1 /. k = vs1 . k by ;
A27: now :: thesis: for n being Nat st S2[n] holds
S2[n + 1]
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A28: S2[n] ; :: thesis: S2[n + 1]
thus S2[n + 1] :: thesis: verum
proof
assume A29: n + 1 in dom c ; :: thesis: ( 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) ) ) )
then A30: 1 <= n + 1 by FINSEQ_3:25;
A31: n + 1 <= len c by ;
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: verum
proof
per cases ( n = 0 or 0 < n ) ;
suppose A32: n = 0 ; :: thesis: ( 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) ) ) )
hence vs1 /. (n + 1) <> vs /. (n + 1) by ; :: thesis: ( 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) ) ) )
A33: 1 <= len c by ;
then c . 1 joins vs /. 1,vs /. (1 + 1) by A1;
then A34: ( ( 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 ) ) ;
c . 1 joins vs1 /. 1,vs1 /. (1 + 1) by ;
hence vs1 /. ((n + 1) + 1) <> vs /. ((n + 1) + 1) by ; :: thesis: ( ( 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) ) )
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 A32; :: thesis: verum
end;
suppose A35: 0 < n ; :: thesis: ( 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) ) ) )
A36: n <= len c by ;
A37: 0 + 1 <= n by ;
hence vs1 /. (n + 1) <> vs /. (n + 1) by ; :: thesis: ( 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) ) ) )
c . n joins vs1 /. n,vs1 /. (n + 1) by ;
then A38: ( ( 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 ) ) ;
c . (n + 1) joins vs /. (n + 1),vs /. ((n + 1) + 1) by A1, A30, A31;
then A39: ( ( 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) ) ) ;
A40: c . (n + 1) joins vs1 /. (n + 1),vs1 /. ((n + 1) + 1) by ;
hence vs1 /. ((n + 1) + 1) <> vs /. ((n + 1) + 1) by ; :: thesis: ( ( 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) ) )
c . n joins vs /. n,vs /. (n + 1) by A1, A37, A36;
hence ( ( 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 ; :: thesis: verum
end;
end;
end;
end;
end;
A41: S2[ 0 ] by FINSEQ_3:25;
A42: for n being Nat holds S2[n] from
now :: thesis: for x being object holds
( ( x in G -VSet (rng c) implies x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} ) & ( x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} implies x in G -VSet (rng c) ) )
let x be object ; :: thesis: ( ( x in G -VSet (rng c) implies x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} ) & ( x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} implies x in G -VSet (rng c) ) )
hereby :: thesis: ( x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} implies x in G -VSet (rng c) )
assume x in G -VSet (rng c) ; :: thesis: x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
then consider v being Element of G such that
A43: x = v and
A44: 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
A45: e in rng c and
A46: ( v = the Source of G . e or v = the Target of G . e ) by A44;
consider d being object such that
A47: d in dom c and
A48: e = c . d by ;
reconsider d = d as Element of NAT by A47;
( ( 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 ;
hence x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by ; :: thesis: verum
end;
0 + 1 <= len c by ;
then A49: 1 in dom c by FINSEQ_3:25;
then A50: c . 1 in rng c by FUNCT_1:def 3;
A51: rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e = c . 1 as Element of the carrier' of G by A50;
reconsider t = the Target of G . e as Element of G by ;
reconsider s = the Source of G . e as Element of G by ;
assume x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} ; :: thesis: x in G -VSet (rng c)
then A52: ( x = s or x = t ) by TARSKI:def 2;
e in rng c by ;
hence x in G -VSet (rng c) by A52; :: thesis: verum
end;
then A53: G -VSet (rng c) = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by TARSKI:2;
c . k joins vs1 /. k,vs1 /. (k + 1) by ;
then A54: ( ( 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 ) ) by A22;
A55: c . k joins vs /. k,vs /. (k + 1) by A1, A22, A24;
A56: now :: thesis: for n being Nat st n in dom c holds
the Source of G . (c . n) <> the Target of G . (c . n)
let n be Nat; :: thesis: ( n in dom c implies the Source of G . (c . n) <> the Target of G . (c . n) )
( 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 A42;
hence ( n in dom c implies the Source of G . (c . n) <> the Target of G . (c . n) ) by A19, A22, A26, A25, A55, A54; :: thesis: verum
end;
( ( 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 ;
then card (G -VSet (rng c)) = 2 by ;
hence contradiction by A13, A24, A56; :: thesis: verum
end;
end;
end;
end;
suppose 1 < k ; :: thesis: contradiction
then 1 + 1 <= k by NAT_1:13;
then consider k1 being Nat such that
A57: 1 <= k1 and
A58: k1 < k and
A59: k = k1 + 1 by FINSEQ_6:127;
A60: k <= len vs1 by ;
then A61: k1 <= len vs1 by ;
then A62: k1 in dom vs1 by ;
A63: k1 <= len c by ;
then c . k1 joins vs1 /. k1,vs1 /. (k1 + 1) by ;
then A64: ( ( 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 ) ) by A59;
A65: vs1 /. k1 = vs1 . k1 by ;
A66: vs1 /. k = vs1 . k by ;
c . k1 joins vs /. k1,vs /. (k1 + 1) by A1, A57, A63;
then A67: ( ( 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 A59;
A68: vs /. k = vs . k by ;
vs /. k1 = vs . k1 by ;
hence contradiction by A19, A20, A58, A62, A65, A66, A68, A64, A67; :: thesis: verum
end;
end;
end;
end;
end;
end;
assume A69: for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs ; :: thesis: ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) )
assume card the carrier of G <> 1 ; :: thesis: ( c <> {} & not c alternates_vertices_in G )
then consider x, y being set such that
A70: x in the carrier of G and
A71: y in the carrier of G and
A72: x <> y by Lm7;
reconsider y = y as Element of G by A71;
reconsider x = x as Element of G by A70;
assume A73: ( c = {} or c alternates_vertices_in G ) ; :: thesis: contradiction
thus contradiction :: thesis: verum
proof
per cases by A73;
suppose c alternates_vertices_in G ; :: thesis: contradiction
then consider vs1, vs2 being FinSequence of the carrier of G such that
A76: vs1 <> vs2 and
A77: vs1 is_vertex_seq_of c and
A78: vs2 is_vertex_seq_of c and
for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) by Th38;
vs1 = vs by ;
hence contradiction by A69, A76, A78; :: thesis: verum
end;
end;
end;