let G be Graph; :: thesis:
let vs1, vs2 be FinSequence of the carrier of G; :: thesis:
let c be Chain of G; :: thesis:
assume that
A1: c <> {} and
A2: vs1 is_vertex_seq_of c and
A3: vs2 is_vertex_seq_of c ; :: thesis:
assume A4: vs1 <> vs2 ; :: thesis:
set SG = the Source of G;
set TG = the Target of G;
A5: ( len vs1 = (len c) + 1 & len vs2 = (len c) + 1 ) by A2, A3, Def7;
defpred S₁[ Nat] means ( $1 in dom vs1 & vs1 . $1 <> vs2 . $1 );
A6: ( Seg (len vs1) = dom vs1 & Seg (len vs2) = dom vs2 ) by FINSEQ_1:def 3;
A7: ex j being Nat st S₁[j] by A4, A5, FINSEQ_2:10;
consider k being Nat such that
A8: S₁[k] and
A9: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A7);
A10: ( 1 <= k & k <= (len c) + 1 ) by A5, A8, FINSEQ_3:27;

per cases by A10, XXREAL_0:1;

suppose A11: k = 1 ; :: thesis:

hence vs1 . 1 <> vs2 . 1 by A8; :: thesis:
let vs be FinSequence of the carrier of G; :: thesis:
assume A12: vs is_vertex_seq_of c ; :: thesis:
then A13: len vs = (len c) + 1 by Def7;
len c <> 0 by A1;
then ( 0 + 1 = 1 & 0 < len c ) ;
then A14: 1 <= len c by NAT_1:13;
A15: 1 <= len vs1 by A5, NAT_1:12;
set v1 = vs /. 1;
set v2 = vs /. (1 + 1);
set v11 = vs1 /. 1;
set v12 = vs1 /. (1 + 1);
set v21 = vs2 /. 1;
A17: ( vs /. 1 = vs . 1 & vs1 /. 1 = vs1 . 1 & vs2 /. 1 = vs2 . 1 ) by A5, A13, A15, FINSEQ_4:24;
A18: c . 1 joins vs /. 1,vs /. (1 + 1) by A12, A14, Def7;
A19: c . 1 joins vs1 /. 1,vs1 /. (1 + 1) by A2, A14, Def7;
A20: c . 1 joins vs2 /. 1,vs2 /. (1 + 1) by A3, A14, Def7;
A21: ( ( vs /. 1 = vs1 /. 1 & vs /. (1 + 1) = vs1 /. (1 + 1) ) or ( vs /. 1 = vs1 /. (1 + 1) & vs /. (1 + 1) = vs1 /. 1 ) ) by A18, A19, Th32;
thus ( vs = vs1 or vs = vs2 ) :: thesis:

proof

per cases by A8, A11, A17, A18, A20, A21, Th32;

suppose A22: vs /. 1 = vs1 /. 1 ; :: thesis:

now

thus len vs = len vs ; :: thesis:
thus len vs1 = len vs by A5, A12, Def7; :: thesis:
defpred S₂[ Nat] means ( $1 in dom vs implies vs . $1 = vs1 . $1 );
A23: S₂[ 0 ] by FINSEQ_3:27;
A24: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume A25: ( i in dom vs implies vs . i = vs1 . i ) ; :: thesis:
assume A26: i + 1 in dom vs ; :: thesis:
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A27: ( 1 <= i + 1 & i + 1 <= len vs ) by A26, FINSEQ_3:27;
A28: ( ( 0 = i or 0 < i ) & 0 + 1 = 1 ) ;

per cases by A28, NAT_1:13;

suppose i = 0 ; :: thesis:

hence vs . (i + 1) = vs1 . (i + 1) by A17, A22; :: thesis:

end;

suppose A29: 1 <= i ; :: thesis:

A30: i <= len c by A13, A27, XREAL_1:8;
then A31: i <= len vs by A13, NAT_1:12;
set v1 = vs /. i;
set v2 = vs /. (i + 1);
set v11 = vs1 /. i;
set v12 = vs1 /. (i + 1);
A32: ( vs /. i = vs . i & vs1 /. i = vs1 . i & vs /. (i + 1) = vs . (i + 1) & vs1 /. (i + 1) = vs1 . (i + 1) ) by A5, A13, A27, A29, A31, FINSEQ_4:24;
A33: c . i joins vs /. i,vs /. (i + 1) by A12, A29, A30, Def7;
c . i joins vs1 /. i,vs1 /. (i + 1) by A2, A29, A30, Def7;
then ( ( vs /. i = vs1 /. i & vs /. (i + 1) = vs1 /. (i + 1) ) or ( vs /. i = vs1 /. (i + 1) & vs /. (i + 1) = vs1 /. i ) ) by A33, Th32;
hence vs . (i + 1) = vs1 . (i + 1) by A25, A29, A31, A32, FINSEQ_3:27; :: thesis:

end;

thus for i being Nat holds S₂[i] from NAT_1:sch 2(A23, A24); :: thesis:

end;

hence ( vs = vs1 or vs = vs2 ) by FINSEQ_2:10; :: thesis:

end;

suppose A34: vs /. 1 = vs2 /. 1 ; :: thesis:

now

thus len vs = len vs ; :: thesis:
thus len vs2 = len vs by A5, A12, Def7; :: thesis:
defpred S₂[ Nat] means ( $1 in dom vs implies vs . $1 = vs2 . $1 );
A35: S₂[ 0 ] by FINSEQ_3:27;
A36: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume A37: ( i in dom vs implies vs . i = vs2 . i ) ; :: thesis:
assume i + 1 in dom vs ; :: thesis:
then A38: ( 1 <= i + 1 & i + 1 <= len vs ) by FINSEQ_3:27;
A39: ( ( 0 = i or 0 < i ) & 0 + 1 = 1 ) ;
reconsider i = i as Element of NAT by ORDINAL1:def 13;

per cases by A39, NAT_1:13;

suppose i = 0 ; :: thesis:

hence vs . (i + 1) = vs2 . (i + 1) by A17, A34; :: thesis:

end;

suppose A40: 1 <= i ; :: thesis:

A41: i <= len c by A13, A38, XREAL_1:8;
then A42: i <= len vs by A13, NAT_1:12;
set v1 = vs /. i;
set v2 = vs /. (i + 1);
set v11 = vs2 /. i;
set v12 = vs2 /. (i + 1);
A43: ( vs /. i = vs . i & vs2 /. i = vs2 . i & vs /. (i + 1) = vs . (i + 1) & vs2 /. (i + 1) = vs2 . (i + 1) ) by A5, A13, A38, A40, A42, FINSEQ_4:24;
A44: c . i joins vs /. i,vs /. (i + 1) by A12, A40, A41, Def7;
c . i joins vs2 /. i,vs2 /. (i + 1) by A3, A40, A41, Def7;
then ( ( vs /. i = vs2 /. i & vs /. (i + 1) = vs2 /. (i + 1) ) or ( vs /. i = vs2 /. (i + 1) & vs /. (i + 1) = vs2 /. i ) ) by A44, Th32;
hence vs . (i + 1) = vs2 . (i + 1) by A37, A40, A42, A43, FINSEQ_3:27; :: thesis:

end;

thus for i being Nat holds S₂[i] from NAT_1:sch 2(A35, A36); :: thesis:

end;

hence ( vs = vs1 or vs = vs2 ) by FINSEQ_2:10; :: thesis:

end;

suppose 1 < k ; :: thesis:

then 1 + 1 <= k by NAT_1:13;
then consider k1 being Element of NAT such that
A45: ( 1 <= k1 & k1 < k & k = k1 + 1 ) by Th1;
A46: k <= len vs1 by A8, FINSEQ_3:27;
then A47: k1 <= len c by A5, A45, XREAL_1:8;
A48: k1 <= len vs1 by A45, A46, XXREAL_0:2;
then A49: k1 in dom vs1 by A45, FINSEQ_3:27;
A50: ( vs1 /. k1 = vs1 . k1 & vs1 /. k = vs1 . k & vs2 /. k1 = vs2 . k1 & vs2 /. k = vs2 . k ) by A5, A6, A8, A45, A48, FINSEQ_4:24, PARTFUN1:def 8;
A51: c . k1 joins vs1 /. k1,vs1 /. (k1 + 1) by A2, A45, A47, Def7;
c . k1 joins vs2 /. k1,vs2 /. (k1 + 1) by A3, A45, A47, Def7;
then ( ( ( 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 ) ) & ( ( 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 A45, A51, GRAPH_1:def 10;
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 A8, A9, A45, A49, A50; :: thesis:

end;