let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ;
consider k being Nat such that
A9: S1[k] and
A10: for n being Nat st S1[n] holds
k <= n from A11: 1 <= k by ;
per cases ( k = 1 or 1 < k ) by ;
suppose A12: k = 1 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( vs = vs1 or vs = vs2 )
then A14: len vs = (len c) + 1 ;
0 + 1 = 1 ;
then A15: 1 <= len c by ;
then A16: c . 1 joins vs /. 1,vs /. (1 + 1) by A13;
c . 1 joins vs1 /. 1,vs1 /. (1 + 1) by ;
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 ;
then A19: vs1 /. 1 = vs1 . 1 by FINSEQ_4:15;
A20: vs2 /. 1 = vs2 . 1 by ;
A21: c . 1 joins vs2 /. 1,vs2 /. (1 + 1) by ;
thus ( vs = vs1 or vs = vs2 ) :: thesis: verum
proof
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 ; :: thesis: ( vs = vs1 or vs = vs2 )
now :: thesis: ( 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 ; :: thesis: ( len vs1 = len vs & ( for i being Nat holds S2[i] ) )
thus len vs1 = len vs by ; :: thesis: 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; :: thesis: ( S2[i] implies S2[i + 1] )
assume A25: ( i in dom vs implies vs . i = vs1 . i ) ; :: thesis: S2[i + 1]
assume A26: i + 1 in dom vs ; :: thesis: vs . (i + 1) = vs1 . (i + 1)
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A27: 1 <= i + 1 by ;
A28: i + 1 <= len vs by ;
per cases ( i = 0 or 1 <= i ) by ;
suppose i = 0 ; :: thesis: vs . (i + 1) = vs1 . (i + 1)
hence vs . (i + 1) = vs1 . (i + 1) by ; :: thesis: verum
end;
suppose A29: 1 <= i ; :: thesis: 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 ;
set v1 = vs /. i;
A31: i <= len c by ;
then A32: c . i joins vs1 /. i,vs1 /. (i + 1) by ;
A33: i <= len vs by ;
then A34: vs /. i = vs . i by ;
c . i joins vs /. i,vs /. (i + 1) by ;
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 ;
hence vs . (i + 1) = vs1 . (i + 1) by ; :: thesis: verum
end;
end;
end;
A36: S2[ 0 ] by FINSEQ_3:25;
thus for i being Nat holds S2[i] from :: thesis: verum
end;
hence ( vs = vs1 or vs = vs2 ) by FINSEQ_2:9; :: thesis: verum
end;
suppose A37: vs /. 1 = vs2 /. 1 ; :: thesis: ( vs = vs1 or vs = vs2 )
now :: thesis: ( 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 ; :: thesis: ( len vs2 = len vs & ( for i being Nat holds S2[i] ) )
thus len vs2 = len vs by ; :: thesis: 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; :: thesis: ( S2[i] implies S2[i + 1] )
assume A40: ( i in dom vs implies vs . i = vs2 . i ) ; :: thesis: S2[i + 1]
assume A41: i + 1 in dom vs ; :: thesis: vs . (i + 1) = vs2 . (i + 1)
then A42: 1 <= i + 1 by FINSEQ_3:25;
A43: i + 1 <= len vs by ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
per cases ( i = 0 or 1 <= i ) by ;
suppose i = 0 ; :: thesis: vs . (i + 1) = vs2 . (i + 1)
hence vs . (i + 1) = vs2 . (i + 1) by ; :: thesis: verum
end;
suppose A44: 1 <= i ; :: thesis: 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 ;
set v1 = vs /. i;
A46: i <= len c by ;
then A47: c . i joins vs2 /. i,vs2 /. (i + 1) by ;
A48: i <= len vs by ;
then A49: vs /. i = vs . i by ;
c . i joins vs /. i,vs /. (i + 1) by ;
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 ;
hence vs . (i + 1) = vs2 . (i + 1) by ; :: thesis: verum
end;
end;
end;
A51: S2[ 0 ] by FINSEQ_3:25;
thus for i being Nat holds S2[i] from :: thesis: verum
end;
hence ( vs = vs1 or vs = vs2 ) by FINSEQ_2:9; :: thesis: verum
end;
end;
end;
end;
suppose 1 < k ; :: thesis: ( 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 ;
then A56: k1 <= len vs1 by ;
then A57: k1 in dom vs1 by ;
A58: vs1 /. k1 = vs1 . k1 by ;
A59: vs2 /. k = vs2 . k by ;
A60: vs1 /. k = vs1 . k by ;
A61: k1 <= len c by ;
then c . k1 joins vs1 /. k1,vs1 /. (k1 + 1) by ;
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 ;
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; :: thesis: verum
end;
end;