let G be Graph; for vs1, vs2 being FinSequence of the carrier of G
for sc being simple Chain of G st 2 < len sc & vs1 is_vertex_seq_of sc & vs2 is_vertex_seq_of sc holds
vs1 = vs2
let vs1, vs2 be FinSequence of the carrier of G; for sc being simple Chain of G st 2 < len sc & vs1 is_vertex_seq_of sc & vs2 is_vertex_seq_of sc holds
vs1 = vs2
let sc be simple Chain of G; ( 2 < len sc & vs1 is_vertex_seq_of sc & vs2 is_vertex_seq_of sc implies vs1 = vs2 )
assume that
A1:
2 < len sc
and
A2:
vs1 is_vertex_seq_of sc
and
A3:
vs2 is_vertex_seq_of sc
; vs1 = vs2
A4:
len vs1 = (len sc) + 1
by A2;
defpred S1[ Nat] means ( $1 in dom vs1 & vs1 . $1 <> vs2 . $1 );
set TG = the Target of G;
set SG = the Source of G;
A5:
Seg (len vs1) = dom vs1
by FINSEQ_1:def 3;
A6:
Seg (len vs2) = dom vs2
by FINSEQ_1:def 3;
A7:
len vs2 = (len sc) + 1
by A3;
assume A8:
vs1 <> vs2
; contradiction
then A9:
ex j being Nat st S1[j]
by A4, A7, FINSEQ_2:9;
consider k being Nat such that
A10:
S1[k]
and
A11:
for n being Nat st S1[n] holds
k <= n
from NAT_1:sch 5(A9);
A12:
1 <= k
by A10, FINSEQ_3:25;
per cases
( k = 1 or 1 < k )
by A12, XXREAL_0:1;
suppose A13:
k = 1
;
contradictionset v23 =
vs2 /. ((1 + 1) + 1);
set v22 =
vs2 /. (1 + 1);
set v21 =
vs2 /. 1;
set v13 =
vs1 /. ((1 + 1) + 1);
set v12 =
vs1 /. (1 + 1);
set v11 =
vs1 /. 1;
A14:
(1 + 1) + 1
<= len vs1
by A1, A4, XREAL_1:6;
then A15:
vs1 /. ((1 + 1) + 1) = vs1 . ((1 + 1) + 1)
by FINSEQ_4:15;
A16:
1
<= len vs1
by A14, XXREAL_0:2;
then A17:
vs1 /. 1
= vs1 . 1
by FINSEQ_4:15;
A18:
1
<= len sc
by A1, XXREAL_0:2;
then A19:
sc . 1
joins vs2 /. 1,
vs2 /. (1 + 1)
by A3;
sc . 1
joins vs1 /. 1,
vs1 /. (1 + 1)
by A2, A18;
then A20:
( (
vs1 /. 1
= vs2 /. 1 &
vs1 /. (1 + 1) = vs2 /. (1 + 1) ) or (
vs1 /. 1
= vs2 /. (1 + 1) &
vs1 /. (1 + 1) = vs2 /. 1 ) )
by A19;
A21:
vs2 /. 1
= vs2 . 1
by A4, A7, A16, FINSEQ_4:15;
consider vs being
FinSequence of the
carrier of
G such that A22:
vs is_vertex_seq_of sc
and A23:
for
n,
m being
Nat st 1
<= n &
n < m &
m <= len vs &
vs . n = vs . m holds
(
n = 1 &
m = len vs )
by Def9;
sc <> {}
by A1;
then A24:
(
vs = vs1 or
vs = vs2 )
by A2, A3, A8, A22, Th34;
A25:
vs2 /. ((1 + 1) + 1) = vs2 . ((1 + 1) + 1)
by A4, A7, A14, FINSEQ_4:15;
A26:
sc . 2
joins vs2 /. (1 + 1),
vs2 /. ((1 + 1) + 1)
by A1, A3;
A27:
sc . 2
joins vs1 /. (1 + 1),
vs1 /. ((1 + 1) + 1)
by A1, A2;
then A28:
vs2 /. 1
= vs2 /. ((1 + 1) + 1)
by A10, A13, A17, A21, A26, A20;
vs1 /. 1
= vs1 /. ((1 + 1) + 1)
by A10, A13, A17, A21, A27, A26, A20;
then
(1 + 1) + 1
= len vs
by A4, A7, A14, A17, A15, A21, A25, A28, A23, A24;
hence
contradiction
by A1, A4, A7, A24;
verum end; suppose
1
< k
;
contradictionthen
1
+ 1
<= k
by NAT_1:13;
then consider k1 being
Nat such that A29:
1
<= k1
and A30:
k1 < k
and A31:
k = k1 + 1
by FINSEQ_6:127;
A32:
k <= len vs1
by A10, FINSEQ_3:25;
then A33:
k1 <= len vs1
by A30, XXREAL_0:2;
then A34:
k1 in dom vs1
by A29, FINSEQ_3:25;
A35:
vs1 /. k1 = vs1 . k1
by A29, A33, FINSEQ_4:15;
A36:
vs2 /. k = vs2 . k
by A4, A7, A5, A6, A10, PARTFUN1:def 6;
A37:
vs1 /. k = vs1 . k
by A10, PARTFUN1:def 6;
A38:
k1 <= len sc
by A4, A31, A32, XREAL_1:6;
then
sc . k1 joins vs1 /. k1,
vs1 /. (k1 + 1)
by A2, A29;
then A39:
( ( the
Source of
G . (sc . k1) = vs1 /. k1 & the
Target of
G . (sc . k1) = vs1 /. k ) or ( the
Source of
G . (sc . k1) = vs1 /. k & the
Target of
G . (sc . k1) = vs1 /. k1 ) )
by A31;
sc . k1 joins vs2 /. k1,
vs2 /. (k1 + 1)
by A3, A29, A38;
then A40:
( ( the
Source of
G . (sc . k1) = vs2 /. k1 & the
Target of
G . (sc . k1) = vs2 /. k ) or ( the
Source of
G . (sc . k1) = vs2 /. k & the
Target of
G . (sc . k1) = vs2 /. k1 ) )
by A31;
vs2 /. k1 = vs2 . k1
by A4, A7, A29, A33, FINSEQ_4:15;
hence
contradiction
by A10, A11, A30, A34, A35, A37, A36, A39, A40;
verum end;