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

A4: len vs1 = (len sc) + 1 by A2;

defpred S_{1}[ 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 ; :: thesis: contradiction

then A9: ex j being Nat st S_{1}[j]
by A4, A7, FINSEQ_2:9;

consider k being Nat such that

A10: S_{1}[k]
and

A11: for n being Nat st S_{1}[n] holds

k <= n from NAT_1:sch 5(A9);

A12: 1 <= k by A10, FINSEQ_3:25;

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

A4: len vs1 = (len sc) + 1 by A2;

defpred S

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 ; :: thesis: contradiction

then A9: ex j being Nat st S

consider k being Nat such that

A10: S

A11: for n being Nat st S

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;

end;

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

set 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; :: thesis: verum

end;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; :: thesis: verum

suppose
1 < k
; :: thesis: contradiction

then
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; :: thesis: verum

end;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; :: thesis: verum