let G be Graph; :: thesis: for sc being simple Chain of G holds
( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )
let sc be simple Chain of G; :: thesis: ( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )

hereby :: thesis: ( ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) implies sc is Path of G )

assume A1: sc is Path of G ; :: thesis: ( not len sc = 0 & not len sc = 1 implies not sc . 1 = sc . 2 )
assume A2: not len sc = 0 ; :: thesis: ( not len sc = 1 implies not sc . 1 = sc . 2 )
assume not len sc = 1 ; :: thesis: not sc . 1 = sc . 2
then len sc > 1 by A2, NAT_1:25;
then A3: 1 + 1 <= len sc by NAT_1:13;
assume sc . 1 = sc . 2 ; :: thesis: contradiction
hence contradiction by A1, A3, GRAPH_1:def 16; :: thesis: verum

end;

assume A4: ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) ; :: thesis: sc is Path of G

per cases ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) by A4;

suppose len sc = 0 ; :: thesis: sc is Path of G

then for n, m being Nat st 1 <= n & n < m & m <= len sc holds
sc . n <> sc . m ;
hence sc is Path of G by GRAPH_1:def 16; :: thesis: verum

end;

suppose len sc = 1 ; :: thesis: sc is Path of G

then for n, m being Nat st 1 <= n & n < m & m <= len sc holds
sc . n <> sc . m by XXREAL_0:2;
hence sc is Path of G by GRAPH_1:def 16; :: thesis: verum

end;

suppose A5: sc . 1 <> sc . 2 ; :: thesis: sc is Path of G

now :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len sc holds
sc . n <> sc . m

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len sc implies sc . n <> sc . m )
assume that
A6: 1 <= n and
A7: n < m and
A8: m <= len sc ; :: thesis: sc . n <> sc . m
thus sc . n <> sc . m :: thesis: verum

proof

consider vs being FinSequence of the carrier of G such that
A9: vs is_vertex_seq_of sc and
A10: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) by Def9;
set vm1 = vs /. (m + 1);
A11: len vs = (len sc) + 1 by A9;
then A12: m + 1 <= len vs by A8, XREAL_1:6;
then A13: vs /. (m + 1) = vs . (m + 1) by FINSEQ_4:15, NAT_1:12;
set vn1 = vs /. (n + 1);
set vn = vs /. n;
A14: n <= len sc by A7, A8, XXREAL_0:2;
then A15: sc . n joins vs /. n,vs /. (n + 1) by A6, A9;
n + 1 <= len vs by A11, A14, XREAL_1:6;
then A16: vs /. (n + 1) = vs . (n + 1) by FINSEQ_4:15, NAT_1:12;
n <= len vs by A11, A14, NAT_1:12;
then A17: vs /. n = vs . n by A6, FINSEQ_4:15;
set vm = vs /. m;
A18: 1 <= m by A6, A7, XXREAL_0:2;
then A19: sc . m joins vs /. m,vs /. (m + 1) by A8, A9;
A20: m <= len vs by A8, A11, NAT_1:12;
then A21: vs /. m = vs . m by A18, FINSEQ_4:15;
assume A22: not sc . n <> sc . m ; :: thesis: contradiction

per cases ( ( vs /. n = vs /. m & vs /. (n + 1) = vs /. (m + 1) ) or ( vs /. n = vs /. (m + 1) & vs /. (n + 1) = vs /. m ) ) by A22, A15, A19;

suppose A23: ( vs /. n = vs /. m & vs /. (n + 1) = vs /. (m + 1) ) ; :: thesis: contradiction

A24: n + 1 < m + 1 by A7, XREAL_1:6;
n = 1 by A6, A7, A10, A20, A17, A21, A23;
hence contradiction by A10, A12, A16, A13, A23, A24; :: thesis: verum

end;

suppose A25: ( vs /. n = vs /. (m + 1) & vs /. (n + 1) = vs /. m ) ; :: thesis: contradiction

thus contradiction :: thesis: verum

proof

A26: n + 1 <= m by A7, NAT_1:13;
A27: n + 0 < m + 1 by A7, XREAL_1:8;

per cases ( n + 1 = m or n + 1 < m ) by A26, XXREAL_0:1;

suppose A28: n + 1 = m ; :: thesis: contradiction

n = 1 by A6, A10, A12, A17, A13, A25, A27;
hence contradiction by A5, A22, A28; :: thesis: verum

end;

suppose A29: n + 1 < m ; :: thesis: contradiction

n = 1 by A6, A10, A12, A17, A13, A25, A27;
hence contradiction by A10, A20, A16, A21, A25, A29; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

hence sc is Path of G by GRAPH_1:def 16; :: thesis: verum

end;

end;