let G be Graph; :: thesis: for vs being FinSequence of the carrier of G

for sc being simple Chain of G st vs is_vertex_seq_of sc holds

for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

let vs be FinSequence of the carrier of G; :: thesis: for sc being simple Chain of G st vs is_vertex_seq_of sc holds

for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

let sc be simple Chain of G; :: thesis: ( vs is_vertex_seq_of sc implies for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) )

assume A1: vs is_vertex_seq_of sc ; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

consider vs1 being FinSequence of the carrier of G such that

A2: vs1 is_vertex_seq_of sc and

A3: for n, m being Nat st 1 <= n & n < m & m <= len vs1 & vs1 . n = vs1 . m holds

( n = 1 & m = len vs1 ) by Def9;

for sc being simple Chain of G st vs is_vertex_seq_of sc holds

for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

let vs be FinSequence of the carrier of G; :: thesis: for sc being simple Chain of G st vs is_vertex_seq_of sc holds

for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

let sc be simple Chain of G; :: thesis: ( vs is_vertex_seq_of sc implies for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) )

assume A1: vs is_vertex_seq_of sc ; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

consider vs1 being FinSequence of the carrier of G such that

A2: vs1 is_vertex_seq_of sc and

A3: for n, m being Nat st 1 <= n & n < m & m <= len vs1 & vs1 . n = vs1 . m holds

( n = 1 & m = len vs1 ) by Def9;

per cases
( len sc <= 2 or 2 < len sc )
;

end;

suppose A4:
len sc <= 2
; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

( n = 1 & m = len vs )

thus
for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) :: thesis: verum

end;( n = 1 & m = len vs ) :: thesis: verum

proof

not not len sc = 0 & ... & not len sc = 2
by A4;

end;per cases then
( len sc = 0 or len sc = 1 or len sc = 2 )
;

end;

suppose A5:
len sc = 0
; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

( n = 1 & m = len vs )

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) )

len vs = 0 + 1 by A1, A5;

hence ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) ) by XXREAL_0:2; :: thesis: verum

end;len vs = 0 + 1 by A1, A5;

hence ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) ) by XXREAL_0:2; :: thesis: verum

suppose
len sc = 1
; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

( n = 1 & m = len vs )

then A6:
len vs = 1 + 1
by A1;

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) )

assume that

A7: 1 <= n and

A8: n < m and

A9: m <= len vs and

vs . n = vs . m ; :: thesis: ( n = 1 & m = len vs )

A10: n + 1 <= m by A8, NAT_1:13;

then n + 1 <= 1 + 1 by A6, A9, XXREAL_0:2;

then n <= 1 by XREAL_1:6;

then n = 1 by A7, XXREAL_0:1;

hence ( n = 1 & m = len vs ) by A6, A9, A10, XXREAL_0:1; :: thesis: verum

end;let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) )

assume that

A7: 1 <= n and

A8: n < m and

A9: m <= len vs and

vs . n = vs . m ; :: thesis: ( n = 1 & m = len vs )

A10: n + 1 <= m by A8, NAT_1:13;

then n + 1 <= 1 + 1 by A6, A9, XXREAL_0:2;

then n <= 1 by XREAL_1:6;

then n = 1 by A7, XXREAL_0:1;

hence ( n = 1 & m = len vs ) by A6, A9, A10, XXREAL_0:1; :: thesis: verum

suppose A11:
len sc = 2
; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

( n = 1 & m = len vs )

set v12 = vs1 /. (1 + 1);

set v2 = vs /. (1 + 1);

set v11 = vs1 /. 1;

A12: sc . 1 joins vs1 /. 1,vs1 /. (1 + 1) by A2, A11;

set v1 = vs /. 1;

sc . 1 joins vs /. 1,vs /. (1 + 1) by A1, A11;

then A13: ( ( vs /. 1 = vs1 /. 1 & vs /. (1 + 1) = vs1 /. (1 + 1) ) or ( vs /. 1 = vs1 /. (1 + 1) & vs /. (1 + 1) = vs1 /. 1 ) ) by A12;

A14: len vs = (1 + 1) + 1 by A1, A11;

then A15: vs /. (1 + 1) = vs . (1 + 1) by FINSEQ_4:15;

set v3 = vs /. ((1 + 1) + 1);

set v13 = vs1 /. ((1 + 1) + 1);

A16: sc . 2 joins vs1 /. (1 + 1),vs1 /. ((1 + 1) + 1) by A2, A11;

sc . 2 joins vs /. (1 + 1),vs /. ((1 + 1) + 1) by A1, A11;

then A17: ( ( vs /. (1 + 1) = vs1 /. (1 + 1) & vs /. ((1 + 1) + 1) = vs1 /. ((1 + 1) + 1) ) or ( vs /. (1 + 1) = vs1 /. ((1 + 1) + 1) & vs /. ((1 + 1) + 1) = vs1 /. (1 + 1) ) ) by A16;

A18: len vs1 = (1 + 1) + 1 by A2, A11;

then A19: vs1 /. 1 = vs1 . 1 by FINSEQ_4:15;

A20: vs1 /. ((1 + 1) + 1) = vs1 . ((1 + 1) + 1) by A18, FINSEQ_4:15;

A21: vs1 /. (1 + 1) = vs1 . (1 + 1) by A18, FINSEQ_4:15;

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) )

assume that

A22: 1 <= n and

A23: n < m and

A24: m <= len vs and

A25: vs . n = vs . m ; :: thesis: ( n = 1 & m = len vs )

n + 1 <= m by A23, NAT_1:13;

then n + 1 <= (1 + 1) + 1 by A14, A24, XXREAL_0:2;

then A26: n <= 1 + 1 by XREAL_1:6;

A27: vs /. ((1 + 1) + 1) = vs . ((1 + 1) + 1) by A14, FINSEQ_4:15;

A28: vs /. 1 = vs . 1 by A14, FINSEQ_4:15;

thus ( n = 1 & m = len vs ) :: thesis: verum

end;set v2 = vs /. (1 + 1);

set v11 = vs1 /. 1;

A12: sc . 1 joins vs1 /. 1,vs1 /. (1 + 1) by A2, A11;

set v1 = vs /. 1;

sc . 1 joins vs /. 1,vs /. (1 + 1) by A1, A11;

then A13: ( ( vs /. 1 = vs1 /. 1 & vs /. (1 + 1) = vs1 /. (1 + 1) ) or ( vs /. 1 = vs1 /. (1 + 1) & vs /. (1 + 1) = vs1 /. 1 ) ) by A12;

A14: len vs = (1 + 1) + 1 by A1, A11;

then A15: vs /. (1 + 1) = vs . (1 + 1) by FINSEQ_4:15;

set v3 = vs /. ((1 + 1) + 1);

set v13 = vs1 /. ((1 + 1) + 1);

A16: sc . 2 joins vs1 /. (1 + 1),vs1 /. ((1 + 1) + 1) by A2, A11;

sc . 2 joins vs /. (1 + 1),vs /. ((1 + 1) + 1) by A1, A11;

then A17: ( ( vs /. (1 + 1) = vs1 /. (1 + 1) & vs /. ((1 + 1) + 1) = vs1 /. ((1 + 1) + 1) ) or ( vs /. (1 + 1) = vs1 /. ((1 + 1) + 1) & vs /. ((1 + 1) + 1) = vs1 /. (1 + 1) ) ) by A16;

A18: len vs1 = (1 + 1) + 1 by A2, A11;

then A19: vs1 /. 1 = vs1 . 1 by FINSEQ_4:15;

A20: vs1 /. ((1 + 1) + 1) = vs1 . ((1 + 1) + 1) by A18, FINSEQ_4:15;

A21: vs1 /. (1 + 1) = vs1 . (1 + 1) by A18, FINSEQ_4:15;

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) )

assume that

A22: 1 <= n and

A23: n < m and

A24: m <= len vs and

A25: vs . n = vs . m ; :: thesis: ( n = 1 & m = len vs )

n + 1 <= m by A23, NAT_1:13;

then n + 1 <= (1 + 1) + 1 by A14, A24, XXREAL_0:2;

then A26: n <= 1 + 1 by XREAL_1:6;

A27: vs /. ((1 + 1) + 1) = vs . ((1 + 1) + 1) by A14, FINSEQ_4:15;

A28: vs /. 1 = vs . 1 by A14, FINSEQ_4:15;

thus ( n = 1 & m = len vs ) :: thesis: verum

proof
end;

per cases
( n = 1 or n = 1 + 1 )
by A22, A26, NAT_1:9;

end;

suppose A29:
n = 1
; :: thesis: ( n = 1 & m = len vs )

1 < m
by A22, A23, XXREAL_0:2;

then A30: 1 + 1 <= m by NAT_1:13;

thus ( n = 1 & m = len vs ) :: thesis: verum

end;then A30: 1 + 1 <= m by NAT_1:13;

thus ( n = 1 & m = len vs ) :: thesis: verum