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 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 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 S_{1}[j]
by A4, A7, FINSEQ_2:9;

consider k being Nat such that

A9: S_{1}[k]
and

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

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

A11: 1 <= k by A9, FINSEQ_3:25;

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 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 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 S

consider k being Nat such that

A9: S

A10: for n being Nat st S

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;

end;

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 ) ) )

( 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

end;( 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
end;

per cases
( vs /. 1 = vs1 /. 1 or vs /. 1 = vs2 /. 1 )
by A9, A12, A19, A20, A16, A21, A17;

end;

suppose A22:
vs /. 1 = vs1 /. 1
; :: thesis: ( vs = vs1 or vs = vs2 )

end;

now :: thesis: ( len vs = len vs & len vs1 = len vs & ( for i being Nat holds S_{2}[i] ) )

hence
( vs = vs1 or vs = vs2 )
by FINSEQ_2:9; :: thesis: verumdefpred S_{2}[ 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 S_{2}[i] ) )

thus len vs1 = len vs by A4, A13; :: thesis: for i being Nat holds S_{2}[i]

A23: for i being Nat st S_{2}[i] holds

S_{2}[i + 1]
_{2}[ 0 ]
by FINSEQ_3:25;

thus for i being Nat holds S_{2}[i]
from NAT_1:sch 2(A36, A23); :: thesis: verum

end;thus len vs = len vs ; :: thesis: ( len vs1 = len vs & ( for i being Nat holds S

thus len vs1 = len vs by A4, A13; :: thesis: for i being Nat holds S

A23: for i being Nat st S

S

proof

A36:
S
A24:
0 + 1 = 1
;

let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume A25: ( i in dom vs implies vs . i = vs1 . i ) ; :: thesis: S_{2}[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;

end;let i be Nat; :: thesis: ( S

assume A25: ( i in dom vs implies vs . i = vs1 . i ) ; :: thesis: S

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;

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;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

thus for i being Nat holds S

suppose A37:
vs /. 1 = vs2 /. 1
; :: thesis: ( vs = vs1 or vs = vs2 )

end;

now :: thesis: ( len vs = len vs & len vs2 = len vs & ( for i being Nat holds S_{2}[i] ) )

hence
( vs = vs1 or vs = vs2 )
by FINSEQ_2:9; :: thesis: verumdefpred S_{2}[ 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 S_{2}[i] ) )

thus len vs2 = len vs by A7, A13; :: thesis: for i being Nat holds S_{2}[i]

A38: for i being Nat st S_{2}[i] holds

S_{2}[i + 1]
_{2}[ 0 ]
by FINSEQ_3:25;

thus for i being Nat holds S_{2}[i]
from NAT_1:sch 2(A51, A38); :: thesis: verum

end;thus len vs = len vs ; :: thesis: ( len vs2 = len vs & ( for i being Nat holds S

thus len vs2 = len vs by A7, A13; :: thesis: for i being Nat holds S

A38: for i being Nat st S

S

proof

A51:
S
A39:
0 + 1 = 1
;

let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume A40: ( i in dom vs implies vs . i = vs2 . i ) ; :: thesis: S_{2}[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;

end;let i be Nat; :: thesis: ( S

assume A40: ( i in dom vs implies vs . i = vs2 . i ) ; :: thesis: S

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;

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;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

thus for i being Nat holds S

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 ) ) )

( 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;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