let G be Graph; for vs1, vs2 being FinSequence of the carrier of G
for c being Chain of G st c <> {} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1 <> vs2 holds
( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )
let vs1, vs2 be FinSequence of the carrier of G; for c being Chain of G st c <> {} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1 <> vs2 holds
( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )
let c be Chain of G; ( c <> {} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1 <> vs2 implies ( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) ) )
assume that
A1:
c <> {}
and
A2:
vs1 is_vertex_seq_of c
and
A3:
vs2 is_vertex_seq_of c
; ( not vs1 <> vs2 or ( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) ) )
A4:
len vs1 = (len c) + 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 c) + 1
by A3;
assume
vs1 <> vs2
; ( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )
then A8:
ex j being Nat st S1[j]
by A4, A7, FINSEQ_2:9;
consider k being Nat such that
A9:
S1[k]
and
A10:
for n being Nat st S1[n] holds
k <= n
from NAT_1:sch 5(A8);
A11:
1 <= k
by A9, FINSEQ_3:25;
per cases
( k = 1 or 1 < k )
by A11, XXREAL_0:1;
suppose A12:
k = 1
;
( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )hence
vs1 . 1
<> vs2 . 1
by A9;
for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 )set v21 =
vs2 /. 1;
set v12 =
vs1 /. (1 + 1);
set v11 =
vs1 /. 1;
let vs be
FinSequence of the
carrier of
G;
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 )set v1 =
vs /. 1;
set v2 =
vs /. (1 + 1);
assume A13:
vs is_vertex_seq_of c
;
( vs = vs1 or vs = vs2 )then A14:
len vs = (len c) + 1
;
0 + 1
= 1
;
then A15:
1
<= len c
by A1, NAT_1:13;
then A16:
c . 1
joins vs /. 1,
vs /. (1 + 1)
by A13;
c . 1
joins vs1 /. 1,
vs1 /. (1 + 1)
by A2, A15;
then A17:
( (
vs /. 1
= vs1 /. 1 &
vs /. (1 + 1) = vs1 /. (1 + 1) ) or (
vs /. 1
= vs1 /. (1 + 1) &
vs /. (1 + 1) = vs1 /. 1 ) )
by A16;
A18:
1
<= len vs1
by A4, NAT_1:12;
then A19:
vs1 /. 1
= vs1 . 1
by FINSEQ_4:15;
A20:
vs2 /. 1
= vs2 . 1
by A4, A7, A18, FINSEQ_4:15;
A21:
c . 1
joins vs2 /. 1,
vs2 /. (1 + 1)
by A3, A15;
thus
(
vs = vs1 or
vs = vs2 )
verumproof
per cases
( vs /. 1 = vs1 /. 1 or vs /. 1 = vs2 /. 1 )
by A9, A12, A19, A20, A16, A21, A17;
suppose A22:
vs /. 1
= vs1 /. 1
;
( vs = vs1 or vs = vs2 )now ( len vs = len vs & len vs1 = len vs & ( for i being Nat holds S2[i] ) )defpred S2[
Nat]
means ( $1
in dom vs implies
vs . $1
= vs1 . $1 );
thus
len vs = len vs
;
( len vs1 = len vs & ( for i being Nat holds S2[i] ) )thus
len vs1 = len vs
by A4, A13;
for i being Nat holds S2[i]A23:
for
i being
Nat st
S2[
i] holds
S2[
i + 1]
proof
A24:
0 + 1
= 1
;
let i be
Nat;
( S2[i] implies S2[i + 1] )
assume A25:
(
i in dom vs implies
vs . i = vs1 . i )
;
S2[i + 1]
assume A26:
i + 1
in dom vs
;
vs . (i + 1) = vs1 . (i + 1)
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
A27:
1
<= i + 1
by A26, FINSEQ_3:25;
A28:
i + 1
<= len vs
by A26, FINSEQ_3:25;
per cases
( i = 0 or 1 <= i )
by A24, NAT_1:13;
suppose A29:
1
<= i
;
vs . (i + 1) = vs1 . (i + 1)set v12 =
vs1 /. (i + 1);
set v11 =
vs1 /. i;
set v2 =
vs /. (i + 1);
A30:
vs /. (i + 1) = vs . (i + 1)
by A27, A28, FINSEQ_4:15;
set v1 =
vs /. i;
A31:
i <= len c
by A14, A28, XREAL_1:6;
then A32:
c . i joins vs1 /. i,
vs1 /. (i + 1)
by A2, A29;
A33:
i <= len vs
by A14, A31, NAT_1:12;
then A34:
vs /. i = vs . i
by A29, FINSEQ_4:15;
c . i joins vs /. i,
vs /. (i + 1)
by A13, A29, A31;
then A35:
( (
vs /. i = vs1 /. i &
vs /. (i + 1) = vs1 /. (i + 1) ) or (
vs /. i = vs1 /. (i + 1) &
vs /. (i + 1) = vs1 /. i ) )
by A32;
vs1 /. i = vs1 . i
by A4, A14, A29, A33, FINSEQ_4:15;
hence
vs . (i + 1) = vs1 . (i + 1)
by A4, A14, A25, A27, A28, A29, A33, A34, A30, A35, FINSEQ_3:25, FINSEQ_4:15;
verum end;
end; A36:
S2[
0 ]
by FINSEQ_3:25;
thus
for
i being
Nat holds
S2[
i]
from NAT_1:sch 2(A36, A23); verum end; hence
(
vs = vs1 or
vs = vs2 )
by FINSEQ_2:9;
verum suppose A37:
vs /. 1
= vs2 /. 1
;
( vs = vs1 or vs = vs2 )now ( len vs = len vs & len vs2 = len vs & ( for i being Nat holds S2[i] ) )defpred S2[
Nat]
means ( $1
in dom vs implies
vs . $1
= vs2 . $1 );
thus
len vs = len vs
;
( len vs2 = len vs & ( for i being Nat holds S2[i] ) )thus
len vs2 = len vs
by A7, A13;
for i being Nat holds S2[i]A38:
for
i being
Nat st
S2[
i] holds
S2[
i + 1]
proof
A39:
0 + 1
= 1
;
let i be
Nat;
( S2[i] implies S2[i + 1] )
assume A40:
(
i in dom vs implies
vs . i = vs2 . i )
;
S2[i + 1]
assume A41:
i + 1
in dom vs
;
vs . (i + 1) = vs2 . (i + 1)
then A42:
1
<= i + 1
by FINSEQ_3:25;
A43:
i + 1
<= len vs
by A41, FINSEQ_3:25;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
per cases
( i = 0 or 1 <= i )
by A39, NAT_1:13;
suppose A44:
1
<= i
;
vs . (i + 1) = vs2 . (i + 1)set v12 =
vs2 /. (i + 1);
set v11 =
vs2 /. i;
set v2 =
vs /. (i + 1);
A45:
vs /. (i + 1) = vs . (i + 1)
by A42, A43, FINSEQ_4:15;
set v1 =
vs /. i;
A46:
i <= len c
by A14, A43, XREAL_1:6;
then A47:
c . i joins vs2 /. i,
vs2 /. (i + 1)
by A3, A44;
A48:
i <= len vs
by A14, A46, NAT_1:12;
then A49:
vs /. i = vs . i
by A44, FINSEQ_4:15;
c . i joins vs /. i,
vs /. (i + 1)
by A13, A44, A46;
then A50:
( (
vs /. i = vs2 /. i &
vs /. (i + 1) = vs2 /. (i + 1) ) or (
vs /. i = vs2 /. (i + 1) &
vs /. (i + 1) = vs2 /. i ) )
by A47;
vs2 /. i = vs2 . i
by A7, A14, A44, A48, FINSEQ_4:15;
hence
vs . (i + 1) = vs2 . (i + 1)
by A7, A14, A40, A42, A43, A44, A48, A49, A45, A50, FINSEQ_3:25, FINSEQ_4:15;
verum end;
end; A51:
S2[
0 ]
by FINSEQ_3:25;
thus
for
i being
Nat holds
S2[
i]
from NAT_1:sch 2(A51, A38); verum end; hence
(
vs = vs1 or
vs = vs2 )
by FINSEQ_2:9;
verum
end; end; suppose
1
< k
;
( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )then
1
+ 1
<= k
by NAT_1:13;
then consider k1 being
Nat such that A52:
1
<= k1
and A53:
k1 < k
and A54:
k = k1 + 1
by FINSEQ_6:127;
A55:
k <= len vs1
by A9, FINSEQ_3:25;
then A56:
k1 <= len vs1
by A53, XXREAL_0:2;
then A57:
k1 in dom vs1
by A52, FINSEQ_3:25;
A58:
vs1 /. k1 = vs1 . k1
by A52, A56, FINSEQ_4:15;
A59:
vs2 /. k = vs2 . k
by A4, A7, A5, A6, A9, PARTFUN1:def 6;
A60:
vs1 /. k = vs1 . k
by A9, PARTFUN1:def 6;
A61:
k1 <= len c
by A4, A54, A55, XREAL_1:6;
then
c . k1 joins vs1 /. k1,
vs1 /. (k1 + 1)
by A2, A52;
then A62:
( ( 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 A54;
c . k1 joins vs2 /. k1,
vs2 /. (k1 + 1)
by A3, A52, A61;
then A63:
( ( the
Source of
G . (c . k1) = vs2 /. k1 & the
Target of
G . (c . k1) = vs2 /. k ) or ( the
Source of
G . (c . k1) = vs2 /. k & the
Target of
G . (c . k1) = vs2 /. k1 ) )
by A54;
vs2 /. k1 = vs2 . k1
by A4, A7, A52, A56, FINSEQ_4:15;
hence
(
vs1 . 1
<> vs2 . 1 & ( for
vs being
FinSequence of the
carrier of
G holds
( not
vs is_vertex_seq_of c or
vs = vs1 or
vs = vs2 ) ) )
by A9, A10, A53, A57, A58, A60, A59, A62, A63;
verum end;