let G be _Graph; :: thesis: for P being Path of G st not P is closed holds
for a, e, b being set st not a in P .vertices() & b = P .first() & e Joins a,b,G holds
(G .walkOf a,e,b) .append P is Path-like
let P be Path of G; :: thesis: ( not P is closed implies for a, e, b being set st not a in P .vertices() & b = P .first() & e Joins a,b,G holds
(G .walkOf a,e,b) .append P is Path-like )
assume A1: not P is closed ; :: thesis: for a, e, b being set st not a in P .vertices() & b = P .first() & e Joins a,b,G holds
(G .walkOf a,e,b) .append P is Path-like
let a, e, b be set ; :: thesis: ( not a in P .vertices() & b = P .first() & e Joins a,b,G implies (G .walkOf a,e,b) .append P is Path-like )
assume that
A2: not a in P .vertices() and
A3: ( b = P .first() & e Joins a,b,G ) ; :: thesis: (G .walkOf a,e,b) .append P is Path-like
set T = G .walkOf a,e,b;
set J = (G .walkOf a,e,b) .append P;
A4: (G .walkOf a,e,b) .last() = P .first() by A3, GLIB_001:16;
3 in Seg 3 by FINSEQ_1:5;
then 3 in Seg (len (G .walkOf a,e,b)) by A3, GLIB_001:15;
then 3 in dom (G .walkOf a,e,b) by FINSEQ_1:def 3;
then ((G .walkOf a,e,b) .append P) . 3 = (G .walkOf a,e,b) . 3 by GLIB_001:33;
then A5: ((G .walkOf a,e,b) .append P) . 3 = (G .walkOf a,e,b) .last() by A3, GLIB_001:15;
then A6: ((G .walkOf a,e,b) .append P) . 3 = b by A3, GLIB_001:16;

A7: now

let m, n be odd Nat; :: thesis: ( m < n & n <= len ((G .walkOf a,e,b) .append P) implies not ((G .walkOf a,e,b) .append P) . m = ((G .walkOf a,e,b) .append P) . n )
assume A8: ( m < n & n <= len ((G .walkOf a,e,b) .append P) ) ; :: thesis: not ((G .walkOf a,e,b) .append P) . m = ((G .walkOf a,e,b) .append P) . n
assume A9: ((G .walkOf a,e,b) .append P) . m = ((G .walkOf a,e,b) .append P) . n ; :: thesis: contradiction
A10: ( 1 <= m & m < len ((G .walkOf a,e,b) .append P) ) by A8, HEYTING3:1, XXREAL_0:2;
then A11: m in dom ((G .walkOf a,e,b) .append P) by FINSEQ_3:27;
(2 * 0 ) + 1 < n by A8, A10, XXREAL_0:2;
then A12: 1 + 2 <= n by Th4;

now

assume m = 1 ; :: thesis: contradiction
then ((G .walkOf a,e,b) .append P) . m = ((G .walkOf a,e,b) .append P) .first() ;
then ((G .walkOf a,e,b) .append P) . m = (G .walkOf a,e,b) .first() by A4, GLIB_001:31;
then A13: not ((G .walkOf a,e,b) .append P) . m in P .vertices() by A2, A3, GLIB_001:16;

per cases ( n = 3 or n > 3 ) by A12, XXREAL_0:1;

suppose n = 3 ; :: thesis: contradiction

hence contradiction by A3, A6, A9, A13, GLIB_001:89; :: thesis: verum

end;

suppose A14: n > 3 ; :: thesis: contradiction

then not n in Seg 3 by FINSEQ_1:3;
then not n in Seg (len (G .walkOf a,e,b)) by A3, GLIB_001:15;
then A15: not n in dom (G .walkOf a,e,b) by FINSEQ_1:def 3;
1 <= n by A14, XXREAL_0:2;
then n in dom ((G .walkOf a,e,b) .append P) by A8, FINSEQ_3:27;
then consider j being Element of NAT such that
A16: ( j < len P & n = (len (G .walkOf a,e,b)) + j ) by A15, GLIB_001:35;
j is even by A16;
then reconsider jj = j as even Nat ;
reconsider j1 = jj + 1 as odd Nat ;
j + 1 <= len P by A16, NAT_1:13;
then P . j1 in P .vertices() by GLIB_001:88;
hence contradiction by A4, A9, A13, A16, GLIB_001:34; :: thesis: verum

end;

end;

end;

then (2 * 0 ) + 1 < m by A10, XXREAL_0:1;
then A17: 1 + 2 <= m by Th4;
then 3 < n by A8, XXREAL_0:2;
then not n in Seg 3 by FINSEQ_1:3;
then not n in Seg (len (G .walkOf a,e,b)) by A3, GLIB_001:15;
then A18: not n in dom (G .walkOf a,e,b) by FINSEQ_1:def 3;
( 1 <= 3 & 3 <= n ) by A8, A17, XXREAL_0:2;
then 1 <= n by XXREAL_0:2;
then n in Seg (len ((G .walkOf a,e,b) .append P)) by A8, FINSEQ_1:3;
then n in dom ((G .walkOf a,e,b) .append P) by FINSEQ_1:def 3;
then consider j being Element of NAT such that
A19: ( j < len P & n = (len (G .walkOf a,e,b)) + j ) by A18, GLIB_001:35;
A20: ((G .walkOf a,e,b) .append P) . n = P . (j + 1) by A4, A19, GLIB_001:34;
j is even by A19;
then reconsider jj = j as even Nat ;
reconsider j1 = jj + 1 as odd Nat ;
A21: j1 <= len P by A19, NAT_1:13;

now

assume m = 3 ; :: thesis: contradiction
then A22: ((G .walkOf a,e,b) .append P) . m = P . 1 by A3, A5, GLIB_001:16;
( 0 <> j & 0 <= j ) by A3, A8, A17, A19, GLIB_001:15;
then (2 * 0 ) + 1 < j1 by XREAL_1:10;
hence contradiction by A1, A9, A20, A21, A22, GLIB_001:148; :: thesis: verum

end;

then 3 < m by A17, XXREAL_0:1;
then not m in Seg 3 by FINSEQ_1:3;
then not m in Seg (len (G .walkOf a,e,b)) by A3, GLIB_001:15;
then not m in dom (G .walkOf a,e,b) by FINSEQ_1:def 3;
then consider k being Element of NAT such that
A23: ( k < len P & m = (len (G .walkOf a,e,b)) + k ) by A11, GLIB_001:35;
A24: ((G .walkOf a,e,b) .append P) . m = P . (k + 1) by A4, A23, GLIB_001:34;
k is even by A23;
then reconsider kk = k as even Nat ;
reconsider k1 = kk + 1 as odd Nat ;
k < j by A8, A19, A23, XREAL_1:9;
then k1 < j1 by XREAL_1:10;
hence contradiction by A1, A9, A20, A21, A24, GLIB_001:148; :: thesis: verum

end;

now

let m, n be odd Element of NAT ; :: thesis: ( m <= len ((G .walkOf a,e,b) .append P) & n <= len ((G .walkOf a,e,b) .append P) & ((G .walkOf a,e,b) .append P) . m = ((G .walkOf a,e,b) .append P) . n implies n = m )
assume A25: ( m <= len ((G .walkOf a,e,b) .append P) & n <= len ((G .walkOf a,e,b) .append P) ) ; :: thesis: ( ((G .walkOf a,e,b) .append P) . m = ((G .walkOf a,e,b) .append P) . n implies n = m )
assume A26: ((G .walkOf a,e,b) .append P) . m = ((G .walkOf a,e,b) .append P) . n ; :: thesis: n = m
then A27: m >= n by A7, A25;
not n < m by A7, A25, A26;
hence n = m by A27, XXREAL_0:1; :: thesis: verum

end;

hence (G .walkOf a,e,b) .append P is Path-like by GLIB_001:147; :: thesis: verum