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 ;
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 ;
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 ;
then A7: ((G .walkOf (a,e,b)) .append P) . 3 = b by ;
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 ;
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 ;
then A14: not ((G .walkOf (a,e,b)) .append P) . m in P .vertices() by ;
per cases ( n = 3 or n > 3 ) by ;
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 ;
then A16: not n in dom (G .walkOf (a,e,b)) by FINSEQ_1:def 3;
1 <= n by ;
then n in dom ((G .walkOf (a,e,b)) .append P) by ;
then consider j being Element of NAT such that
A17: j < len P and
A18: n = (len (G .walkOf (a,e,b))) + j by ;
reconsider jj = j as even Nat by A18;
reconsider j1 = jj + 1 as odd Nat ;
j + 1 <= len P by ;
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 ;
then A19: 1 + 2 <= m by Th4;
then 3 <= n by ;
then 1 <= n by XXREAL_0:2;
then n in Seg (len ((G .walkOf (a,e,b)) .append P)) by ;
then A20: n in dom ((G .walkOf (a,e,b)) .append P) by FINSEQ_1:def 3;
3 < n by ;
then not n in Seg 3 by FINSEQ_1:1;
then not n in Seg (len (G .walkOf (a,e,b))) by ;
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 ;
reconsider jj = j as even Nat by A22;
reconsider j1 = jj + 1 as odd Nat ;
A23: j1 <= len P by ;
m < len ((G .walkOf (a,e,b)) .append P) by ;
then A24: m in dom ((G .walkOf (a,e,b)) .append P) by ;
A25: ((G .walkOf (a,e,b)) .append P) . n = P . (j + 1) by ;
now :: thesis: not m = 3
assume m = 3 ; :: thesis: contradiction
then A26: ((G .walkOf (a,e,b)) .append P) . m = P . 1 by ;
0 <> j by ;
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 ;
then not m in Seg 3 by FINSEQ_1:1;
then not m in Seg (len (G .walkOf (a,e,b))) by ;
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 ;
reconsider kk = k as even Nat by A28;
reconsider k1 = kk + 1 as odd Nat ;
k < j by ;
then A29: k1 < j1 by XREAL_1:8;
((G .walkOf (a,e,b)) .append P) . m = P . (k + 1) by ;
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 ;
m >= n by A8, A31, A32;
hence n = m by ; :: thesis: verum
end;
hence (G .walkOf (a,e,b)) .append P is Path-like by GLIB_001:146; :: thesis: verum