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;

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

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 )

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

proof

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

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

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 )

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;

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 )

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;

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 )

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

proof

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

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

proof

per cases ( m = 1 + 1 or m = (1 + 1) + 1 ) by A14, A24, A30, NAT_1:9;

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

hence ( n = 1 & m = len vs ) by A3, A18, A28, A15, A19, A21, A13, A25, A29; :: thesis: verum

end;

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

hence ( n = 1 & m = len vs ) by A1, A11, A29; :: thesis: verum

end;

end;

end;

end;

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

then (1 + 1) + 1 <= m by A23, NAT_1:13;
then m = (1 + 1) + 1 by A14, A24, XXREAL_0:1;
hence ( n = 1 & m = len vs ) by A3, A18, A15, A27, A21, A20, A17, A25, A31; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose 2 < len 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 )

then vs = vs1 by A1, A2, Th46;
hence for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) by A3; :: thesis: verum

end;

end;