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 Element of 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 Element of 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 Element of 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 Element of 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 & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs1 & vs1 . n = vs1 . m holds
( n = 1 & m = len vs1 ) ) ) by Def10;

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

suppose A3: len sc <= 2 ; :: thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )

thus for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) :: thesis: verum

proof

per cases ( len sc = 0 or len sc = 1 or len sc = 2 ) by A3, NAT_1:27;

suppose len sc = 0 ; :: thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )

then A4: len vs = 0 + 1 by A1, Def7;
let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) )
thus ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) ) by A4, XXREAL_0:2; :: thesis: verum

end;

suppose len sc = 1 ; :: thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )

then A5: ( len vs = 1 + 1 & len vs1 = 1 + 1 ) by A1, A2, Def7;
let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) )
assume that
A6: 1 <= n and
A7: n < m and
A8: m <= len vs and
vs . n = vs . m ; :: thesis: ( n = 1 & m = len vs )
A9: n + 1 <= m by A7, NAT_1:13;
then n + 1 <= 1 + 1 by A5, A8, XXREAL_0:2;
then n <= 1 by XREAL_1:8;
then n = 1 by A6, XXREAL_0:1;
hence ( n = 1 & m = len vs ) by A5, A8, A9, XXREAL_0:1; :: thesis: verum

end;

suppose A10: len sc = 2 ; :: thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )

then A11: ( len vs = (1 + 1) + 1 & len vs1 = (1 + 1) + 1 ) by A1, A2, Def7;
set v1 = vs /. 1;
set v2 = vs /. (1 + 1);
set v3 = vs /. ((1 + 1) + 1);
set v11 = vs1 /. 1;
set v12 = vs1 /. (1 + 1);
set v13 = vs1 /. ((1 + 1) + 1);
A12: ( vs /. 1 = vs . 1 & vs /. (1 + 1) = vs . (1 + 1) & vs /. ((1 + 1) + 1) = vs . ((1 + 1) + 1) & vs1 /. 1 = vs1 . 1 & vs1 /. (1 + 1) = vs1 . (1 + 1) & vs1 /. ((1 + 1) + 1) = vs1 . ((1 + 1) + 1) ) by A11, FINSEQ_4:24;
A13: ( sc . 1 joins vs /. 1,vs /. (1 + 1) & sc . 1 joins vs1 /. 1,vs1 /. (1 + 1) & sc . 2 joins vs /. (1 + 1),vs /. ((1 + 1) + 1) & sc . 2 joins vs1 /. (1 + 1),vs1 /. ((1 + 1) + 1) ) by A1, A2, A10, Def7;
then A14: ( ( vs /. 1 = vs1 /. 1 & vs /. (1 + 1) = vs1 /. (1 + 1) ) or ( vs /. 1 = vs1 /. (1 + 1) & vs /. (1 + 1) = vs1 /. 1 ) ) by Th32;
A15: ( ( 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 A13, Th32;
let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len vs & vs . n = vs . m implies ( n = 1 & m = len vs ) )
assume that
A16: 1 <= n and
A17: n < m and
A18: m <= len vs and
A19: vs . n = vs . m ; :: thesis: ( n = 1 & m = len vs )
n + 1 <= m by A17, NAT_1:13;
then n + 1 <= (1 + 1) + 1 by A11, A18, XXREAL_0:2;
then A20: n <= 1 + 1 by XREAL_1:8;
thus ( n = 1 & m = len vs ) :: thesis: verum

proof

per cases ( n = 1 or n = 1 + 1 ) by A16, A20, NAT_1:9;

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

1 < m by A16, A17, XXREAL_0:2;
then A22: 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 A11, A18, A22, NAT_1:9;

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

hence ( n = 1 & m = len vs ) by A2, A11, A12, A14, A19, A21; :: thesis: verum

end;

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

hence ( n = 1 & m = len vs ) by A1, A10, A21, Def7; :: thesis: verum

end;

end;

end;

end;

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

then (1 + 1) + 1 <= m by A17, NAT_1:13;
then m = (1 + 1) + 1 by A11, A18, XXREAL_0:1;
hence ( n = 1 & m = len vs ) by A2, A11, A12, A15, A19, A23; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose 2 < len sc ; :: thesis: for n, m being Element of 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, Th50;
hence for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) by A2; :: thesis: verum

end;

end;