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;

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

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;

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;

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;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

then
(2 * 0) + 1 < m
by A12, XXREAL_0: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;

end;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;

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;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

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

then
3 < m
by A19, XXREAL_0:1;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 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

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

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

hence
(G .walkOf (a,e,b)) .append P is Path-like
by GLIB_001:146; :: thesis: verumn = 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;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