let G be _Graph; :: thesis: for P being Path of G st P is open 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: ( P is open 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: P is open ; :: 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() and
A4: e Joins a,b,G ; :: thesis: (G .walkOf (a,e,b)) .append P is Path-like
set T = G .walkOf (a,e,b);
A5: (G .walkOf (a,e,b)) .last() = P .first() by A3, A4, GLIB_001:15;
set J = (G .walkOf (a,e,b)) .append P;
3 in Seg 3 by FINSEQ_1:3;
then 3 in Seg (len (G .walkOf (a,e,b))) by A4, GLIB_001:14;
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:32;
then A6: ((G .walkOf (a,e,b)) .append P) . 3 = (G .walkOf (a,e,b)) .last() by A4, GLIB_001:14;
then A7: ((G .walkOf (a,e,b)) .append P) . 3 = b by A4, GLIB_001:15;

A8: now :: thesis: for m, n being odd Nat st m < n & n <= len ((G .walkOf (a,e,b)) .append P) holds
not ((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . n

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 that
A9: m < n and
A10: 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 A11: ((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . n ; :: thesis: contradiction
A12: 1 <= m by ABIAN:12;
then (2 * 0) + 1 < n by A9, XXREAL_0:2;
then A13: 1 + 2 <= n by Th4;

now :: thesis: not m = 1

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 A5, GLIB_001:30;
then A14: not ((G .walkOf (a,e,b)) .append P) . m in P .vertices() by A2, A4, GLIB_001:15;

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

suppose n = 3 ; :: thesis: contradiction

hence contradiction by A3, A7, A11, A14, GLIB_001:88; :: thesis: verum

end;

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

then not n in Seg 3 by FINSEQ_1:1;
then not n in Seg (len (G .walkOf (a,e,b))) by A4, GLIB_001:14;
then A16: not n in dom (G .walkOf (a,e,b)) by FINSEQ_1:def 3;
1 <= n by A15, XXREAL_0:2;
then n in dom ((G .walkOf (a,e,b)) .append P) by A10, FINSEQ_3:25;
then consider j being Element of NAT such that
A17: j < len P and
A18: n = (len (G .walkOf (a,e,b))) + j by A16, GLIB_001:34;
reconsider jj = j as even Nat by A18;
reconsider j1 = jj + 1 as odd Nat ;
j + 1 <= len P by A17, NAT_1:13;
then P . j1 in P .vertices() by GLIB_001:87;
hence contradiction by A5, A11, A14, A17, A18, GLIB_001:33; :: thesis: verum

end;

end;

end;

then (2 * 0) + 1 < m by A12, XXREAL_0:1;
then A19: 1 + 2 <= m by Th4;
then 3 <= n by A9, XXREAL_0:2;
then 1 <= n by XXREAL_0:2;
then n in Seg (len ((G .walkOf (a,e,b)) .append P)) by A10, FINSEQ_1:1;
then A20: n in dom ((G .walkOf (a,e,b)) .append P) by FINSEQ_1:def 3;
3 < n by A9, A19, XXREAL_0:2;
then not n in Seg 3 by FINSEQ_1:1;
then not n in Seg (len (G .walkOf (a,e,b))) by A4, GLIB_001:14;
then not n in dom (G .walkOf (a,e,b)) by FINSEQ_1:def 3;
then consider j being Element of NAT such that
A21: j < len P and
A22: n = (len (G .walkOf (a,e,b))) + j by A20, GLIB_001:34;
reconsider jj = j as even Nat by A22;
reconsider j1 = jj + 1 as odd Nat ;
A23: j1 <= len P by A21, NAT_1:13;
m < len ((G .walkOf (a,e,b)) .append P) by A9, A10, XXREAL_0:2;
then A24: m in dom ((G .walkOf (a,e,b)) .append P) by A12, FINSEQ_3:25;
A25: ((G .walkOf (a,e,b)) .append P) . n = P . (j + 1) by A5, A21, A22, GLIB_001:33;

now :: thesis: not m = 3

assume m = 3 ; :: thesis: contradiction
then A26: ((G .walkOf (a,e,b)) .append P) . m = P . 1 by A3, A4, A6, GLIB_001:15;
0 <> j by A4, A9, A19, A22, GLIB_001:14;
then (2 * 0) + 1 < j1 by XREAL_1:8;
hence contradiction by A1, A11, A25, A23, A26, GLIB_001:147; :: thesis: verum

end;

then 3 < m by A19, XXREAL_0:1;
then not m in Seg 3 by FINSEQ_1:1;
then not m in Seg (len (G .walkOf (a,e,b))) by A4, GLIB_001:14;
then not m in dom (G .walkOf (a,e,b)) by FINSEQ_1:def 3;
then consider k being Element of NAT such that
A27: k < len P and
A28: m = (len (G .walkOf (a,e,b))) + k by A24, GLIB_001:34;
reconsider kk = k as even Nat by A28;
reconsider k1 = kk + 1 as odd Nat ;
k < j by A9, A22, A28, XREAL_1:7;
then A29: k1 < j1 by XREAL_1:8;
((G .walkOf (a,e,b)) .append P) . m = P . (k + 1) by A5, A27, A28, GLIB_001:33;
hence contradiction by A1, A11, A25, A23, A29, GLIB_001:147; :: thesis: verum

end;

now :: thesis: for m, n being odd Element of NAT st 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 holds
n = m

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 that
A30: m <= len ((G .walkOf (a,e,b)) .append P) and
A31: 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 A32: ((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . n ; :: thesis: n = m
then A33: not n < m by A8, A30;
m >= n by A8, A31, A32;
hence n = m by A33, XXREAL_0:1; :: thesis: verum

end;

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