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 )

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

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 A69:
for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds ( 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

end;not vs1 <> vs

per cases
( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) )
by A2;

end;

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

not vs1 <> vs

then reconsider tVG = the carrier of G as finite set ;

consider X being object such that

A4: tVG = {X} by A3, CARD_2:42;

A5: rng vs c= {X} by A4, FINSEQ_1:def 4;

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 A8, A6, FINSEQ_2:9;

vs . j in rng vs by A9, FUNCT_1:def 3;

then A11: vs . j = X by A5, TARSKI:def 1;

A12: rng vs1 c= {X} by A4, FINSEQ_1:def 4;

Seg (len vs1) = dom vs1 by FINSEQ_1:def 3;

then vs1 . j in rng vs1 by A8, A6, A7, A9, FUNCT_1:def 3;

hence contradiction by A10, A12, A11, TARSKI:def 1; :: thesis: verum

end;consider X being object such that

A4: tVG = {X} by A3, CARD_2:42;

A5: rng vs c= {X} by A4, FINSEQ_1:def 4;

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 A8, A6, FINSEQ_2:9;

vs . j in rng vs by A9, FUNCT_1:def 3;

then A11: vs . j = X by A5, TARSKI:def 1;

A12: rng vs1 c= {X} by A4, FINSEQ_1:def 4;

Seg (len vs1) = dom vs1 by FINSEQ_1:def 3;

then vs1 . j in rng vs1 by A8, A6, A7, A9, FUNCT_1:def 3;

hence contradiction by A10, A12, A11, TARSKI:def 1; :: thesis: verum

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

vs1 = vs

thus
for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds

vs1 = vs :: thesis: verum

end;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 S_{1}[ 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 A15, FINSEQ_3:29;

assume vs1 <> vs ; :: thesis: contradiction

then A18: ex i being Nat st S_{1}[i]
by A15, A16, FINSEQ_2:9;

consider k being Nat such that

A19: S_{1}[k]
and

A20: for n being Nat st S_{1}[n] holds

k <= n from NAT_1:sch 5(A18);

A21: ( ( 0 + 1 = 1 & k = 0 ) or 0 + 1 <= k ) by NAT_1:13;

end;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 S

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 A15, FINSEQ_3:29;

assume vs1 <> vs ; :: thesis: contradiction

then A18: ex i being Nat st S

consider k being Nat such that

A19: S

A20: for n being Nat st S

k <= n from NAT_1:sch 5(A18);

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 A21, XXREAL_0:1;

end;

suppose A22:
k = 1
; :: thesis: contradiction

thus
contradiction
:: thesis: verum

end;proof

A23:
0 + 1 = 1
;

end;per cases
( len c = 0 or 1 <= len c )
by A23, NAT_1:13;

end;

suppose A24:
1 <= len c
; :: thesis: contradiction

defpred S_{2}[ 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 A17, A19, PARTFUN1:def 6;

A26: vs1 /. k = vs1 . k by A19, PARTFUN1:def 6;

_{2}[ 0 ]
by FINSEQ_3:25;

A42: for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A41, A27);

c . k joins vs1 /. k,vs1 /. (k + 1) by A14, A22, A24;

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;

then card (G -VSet (rng c)) = 2 by A19, A22, A26, A25, A54, A53, CARD_2:57;

hence contradiction by A13, A24, A56; :: thesis: verum

end;A25: vs /. k = vs . k by A17, A19, PARTFUN1:def 6;

A26: vs1 /. k = vs1 . k by A19, PARTFUN1:def 6;

A27: now :: thesis: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

A41:
SS

let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A28: S_{2}[n]
; :: thesis: S_{2}[n + 1]

thus S_{2}[n + 1]
:: thesis: verum

end;assume A28: S

thus S

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 A29, FINSEQ_3:25;

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

end;then A30: 1 <= n + 1 by FINSEQ_3:25;

A31: n + 1 <= len c by A29, FINSEQ_3:25;

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
end;

per cases
( n = 0 or 0 < n )
;

end;

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 A17, A19, A22, A26, PARTFUN1:def 6; :: 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 A30, A31, XXREAL_0:2;

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 A14, A33;

hence vs1 /. ((n + 1) + 1) <> vs /. ((n + 1) + 1) by A17, A19, A22, A26, A32, A34, PARTFUN1:def 6; :: 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;A33: 1 <= len c by A30, A31, XXREAL_0:2;

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 A14, A33;

hence vs1 /. ((n + 1) + 1) <> vs /. ((n + 1) + 1) by A17, A19, A22, A26, A32, A34, PARTFUN1:def 6; :: 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

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 A31, NAT_1:13;

A37: 0 + 1 <= n by A35, NAT_1:13;

hence vs1 /. (n + 1) <> vs /. (n + 1) by A28, A36, FINSEQ_3:25; :: 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 A14, A37, A36;

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 A14, A30, A31;

hence vs1 /. ((n + 1) + 1) <> vs /. ((n + 1) + 1) by A28, A37, A36, A39, FINSEQ_3:25; :: 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 A28, A37, A36, A38, A40, A39, FINSEQ_3:25; :: thesis: verum

end;A37: 0 + 1 <= n by A35, NAT_1:13;

hence vs1 /. (n + 1) <> vs /. (n + 1) by A28, A36, FINSEQ_3:25; :: 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 A14, A37, A36;

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 A14, A30, A31;

hence vs1 /. ((n + 1) + 1) <> vs /. ((n + 1) + 1) by A28, A37, A36, A39, FINSEQ_3:25; :: 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 A28, A37, A36, A38, A40, A39, FINSEQ_3:25; :: thesis: verum

A42: for n being Nat holds S

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) ) )

then A53:
G -VSet (rng c) = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by TARSKI:2;( ( 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) ) )

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 A50, A51, FUNCT_2:5;

reconsider s = the Source of G . e as Element of G by A50, A51, FUNCT_2:5;

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 A49, FUNCT_1:def 3;

hence x in G -VSet (rng c) by A52; :: thesis: verum

end;hereby :: thesis: ( x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} implies x in G -VSet (rng c) )

0 + 1 <= len c
by A13, NAT_1:13;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 A45, FUNCT_1:def 3;

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 A42, A47;

hence x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A43, A46, A48, TARSKI:def 2; :: thesis: verum

end;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 A45, FUNCT_1:def 3;

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 A42, A47;

hence x in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A43, A46, A48, TARSKI:def 2; :: thesis: verum

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 A50, A51, FUNCT_2:5;

reconsider s = the Source of G . e as Element of G by A50, A51, FUNCT_2:5;

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 A49, FUNCT_1:def 3;

hence x in G -VSet (rng c) by A52; :: thesis: verum

c . k joins vs1 /. k,vs1 /. (k + 1) by A14, A22, A24;

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)

( ( 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 A22, A55;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;( 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

then card (G -VSet (rng c)) = 2 by A19, A22, A26, A25, A54, A53, CARD_2:57;

hence contradiction by A13, A24, A56; :: thesis: verum

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 A19, FINSEQ_3:25;

then A61: k1 <= len vs1 by A58, XXREAL_0:2;

then A62: k1 in dom vs1 by A57, FINSEQ_3:25;

A63: k1 <= len c by A15, A59, A60, XREAL_1:6;

then c . k1 joins vs1 /. k1,vs1 /. (k1 + 1) by A14, A57;

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 A57, A61, FINSEQ_4:15;

A66: vs1 /. k = vs1 . k by A19, PARTFUN1:def 6;

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 A17, A19, PARTFUN1:def 6;

vs /. k1 = vs . k1 by A15, A16, A57, A61, FINSEQ_4:15;

hence contradiction by A19, A20, A58, A62, A65, A66, A68, A64, A67; :: thesis: verum

end;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 A19, FINSEQ_3:25;

then A61: k1 <= len vs1 by A58, XXREAL_0:2;

then A62: k1 in dom vs1 by A57, FINSEQ_3:25;

A63: k1 <= len c by A15, A59, A60, XREAL_1:6;

then c . k1 joins vs1 /. k1,vs1 /. (k1 + 1) by A14, A57;

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 A57, A61, FINSEQ_4:15;

A66: vs1 /. k = vs1 . k by A19, PARTFUN1:def 6;

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 A17, A19, PARTFUN1:def 6;

vs /. k1 = vs . k1 by A15, A16, A57, A61, FINSEQ_4:15;

hence contradiction by A19, A20, A58, A62, A65, A66, A68, A64, A67; :: thesis: verum

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
end;

per cases
( c = {} or c alternates_vertices_in G )
by A73;

end;

suppose A74:
c = {}
; :: thesis: contradiction

then
<*x*> = vs
by A69, Th32;

then A75: vs . 1 = x by FINSEQ_1:40;

<*y*> = vs by A69, A74, Th32;

hence contradiction by A72, A75, FINSEQ_1:40; :: thesis: verum

end;then A75: vs . 1 = x by FINSEQ_1:40;

<*y*> = vs by A69, A74, Th32;

hence contradiction by A72, A75, FINSEQ_1:40; :: thesis: verum

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 A69, A77;

hence contradiction by A69, A76, A78; :: thesis: verum

end;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 A69, A77;

hence contradiction by A69, A76, A78; :: thesis: verum