let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: vs1 = vs2
assume A4: vs1 <> vs2 ; :: thesis: contradiction
set SG = the Source of G;
set TG = the Target of G;
A5: ( len vs1 = (len sc) + 1 & len vs2 = (len sc) + 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 sc) + 1 ) by A5, A8, FINSEQ_3:27;

per cases ( k = 1 or 1 < k ) by A10, XXREAL_0:1;

suppose A11: k = 1 ; :: thesis: contradiction

A12: (1 + 1) + 1 <= len vs1 by A1, A5, XREAL_1:8;
then A13: ( 1 <= len vs1 & 1 + 1 <= len vs1 ) by XXREAL_0:2;
set v11 = vs1 /. 1;
set v12 = vs1 /. (1 + 1);
set v13 = vs1 /. ((1 + 1) + 1);
set v21 = vs2 /. 1;
set v22 = vs2 /. (1 + 1);
set v23 = vs2 /. ((1 + 1) + 1);
A14: ( vs1 /. 1 = vs1 . 1 & vs1 /. (1 + 1) = vs1 . (1 + 1) & vs1 /. ((1 + 1) + 1) = vs1 . ((1 + 1) + 1) & vs2 /. 1 = vs2 . 1 & vs2 /. (1 + 1) = vs2 . (1 + 1) & vs2 /. ((1 + 1) + 1) = vs2 . ((1 + 1) + 1) ) by A5, A12, A13, FINSEQ_4:24;
( 1 + 1 <= len sc & 1 <= len sc ) by A1, XXREAL_0:2;
then A15: ( sc . 1 joins vs1 /. 1,vs1 /. (1 + 1) & sc . 1 joins vs2 /. 1,vs2 /. (1 + 1) & sc . 2 joins vs1 /. (1 + 1),vs1 /. ((1 + 1) + 1) & sc . 2 joins vs2 /. (1 + 1),vs2 /. ((1 + 1) + 1) ) by A2, A3, Def7;
then ( ( vs1 /. 1 = vs2 /. 1 & vs1 /. (1 + 1) = vs2 /. (1 + 1) ) or ( vs1 /. 1 = vs2 /. (1 + 1) & vs1 /. (1 + 1) = vs2 /. 1 ) ) by Th32;
then A16: ( vs1 /. 1 = vs1 /. ((1 + 1) + 1) & vs2 /. 1 = vs2 /. ((1 + 1) + 1) ) by A8, A11, A14, A15, Th32;
consider vs being FinSequence of the carrier of G such that
A17: ( vs is_vertex_seq_of sc & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) ) ) by Def10;
sc <> {} by A1;
then A18: ( vs = vs1 or vs = vs2 ) by A2, A3, A4, A17, Th37;
then (1 + 1) + 1 = len vs by A5, A12, A14, A16, A17;
hence contradiction by A1, A5, A18; :: thesis: verum

end;

suppose 1 < k ; :: thesis: contradiction

then 1 + 1 <= k by NAT_1:13;
then consider k1 being Element of NAT such that
A19: ( 1 <= k1 & k1 < k & k = k1 + 1 ) by Th1;
A20: k <= len vs1 by A8, FINSEQ_3:27;
then A21: k1 <= len sc by A5, A19, XREAL_1:8;
A22: k1 <= len vs1 by A19, A20, XXREAL_0:2;
then A23: k1 in dom vs1 by A19, FINSEQ_3:27;
A24: ( vs1 /. k1 = vs1 . k1 & vs1 /. k = vs1 . k & vs2 /. k1 = vs2 . k1 & vs2 /. k = vs2 . k ) by A5, A6, A8, A19, A22, FINSEQ_4:24, PARTFUN1:def 8;
A25: sc . k1 joins vs1 /. k1,vs1 /. (k1 + 1) by A2, A19, A21, Def7;
sc . k1 joins vs2 /. k1,vs2 /. (k1 + 1) by A3, A19, A21, Def7;
then ( ( ( 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 ) ) & ( ( 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 A19, A25, GRAPH_1:def 10;
hence contradiction by A8, A9, A19, A23, A24; :: thesis: verum

end;

end;