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 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 ; :: 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 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 ) :: 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 A4, A13; :: 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 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 i = 0 ; :: thesis: vs . (i + 1) = vs1 . (i + 1)
hence vs . (i + 1) = vs1 . (i + 1) by A4, A14, A18, A19, A22, FINSEQ_4:15; :: 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 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; :: thesis: verum
end;
end;
end;
A36: S2[ 0 ] by FINSEQ_3:25;
thus for i being Nat holds S2[i] from NAT_1:sch 2(A36, A23); :: 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 A7, A13; :: 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 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 i = 0 ; :: thesis: vs . (i + 1) = vs2 . (i + 1)
hence vs . (i + 1) = vs2 . (i + 1) by A4, A14, A18, A20, A37, FINSEQ_4:15; :: 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 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; :: thesis: verum
end;
end;
end;
A51: S2[ 0 ] by FINSEQ_3:25;
thus for i being Nat holds S2[i] from NAT_1:sch 2(A51, A38); :: 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 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; :: thesis: verum
end;
end;