let G be Graph; 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; 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; ( 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
; ( ( 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 ( 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 ) )
;
for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
not vs1 <> vsper 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
;
for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
not vs1 <> vsthen 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;
( 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
;
not vs1 <> vsthen A8:
len vs1 = (len c) + 1
;
assume
vs1 <> vs
;
contradictionthen 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;
verum end; suppose A13:
(
c <> {} & not
c alternates_vertices_in G )
;
for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vsthus
for
vs1 being
FinSequence of the
carrier of
G st
vs1 is_vertex_seq_of c holds
vs1 = vs
verumproof
set TG = the
Target of
G;
set SG = the
Source of
G;
let vs1 be
FinSequence of the
carrier of
G;
( 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
;
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
;
contradiction
then A18:
ex
i being
Nat st
S1[
i]
by A15, A16, FINSEQ_2:9;
consider k being
Nat such that A19:
S1[
k]
and A20:
for
n being
Nat st
S1[
n] holds
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;
suppose A22:
k = 1
;
contradictionthus
contradiction
verumproof
A23:
0 + 1
= 1
;
per cases
( len c = 0 or 1 <= len c )
by A23, NAT_1:13;
suppose A24:
1
<= len c
;
contradictiondefpred 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 A17, A19, PARTFUN1:def 6;
A26:
vs1 /. k = vs1 . k
by A19, PARTFUN1:def 6;
A27:
now for n being Nat st S2[n] holds
S2[n + 1]let n be
Nat;
( S2[n] implies S2[n + 1] )assume A28:
S2[
n]
;
S2[n + 1]thus
S2[
n + 1]
verumproof
assume A29:
n + 1
in dom c
;
( 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) ) ) )
verumproof
per cases
( n = 0 or 0 < n )
;
suppose A32:
n = 0
;
( 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;
( 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;
( ( 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;
verum end; suppose A35:
0 < n
;
( 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;
( 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;
( ( 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;
verum end;
end;
end; end; A41:
S2[
0 ]
by FINSEQ_3:25;
A42:
for
n being
Nat holds
S2[
n]
from NAT_1:sch 2(A41, A27);
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 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;
( ( 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;
then
card (G -VSet (rng c)) = 2
by A19, A22, A26, A25, A54, A53, CARD_2:57;
hence
contradiction
by A13, A24, A56;
verum end;
end; end; suppose
1
< k
;
contradictionthen
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;
verum 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
; ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) )
assume
card the carrier of G <> 1
; ( 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 )
; contradiction
thus
contradiction
verum