let G be finite _Graph; :: thesis: for W being Path of G holds len (W .vertexSeq()) <= (G .order()) + 1
let W be Path of G; :: thesis: len (W .vertexSeq()) <= (G .order()) + 1

now

per cases ( len W = 1 or len W <> 1 ) ;

suppose len W = 1 ; :: thesis: len (W .vertexSeq()) <= (G .order()) + 1

then 1 + 1 = 2 * (len (W .vertexSeq())) by Def14;
hence len (W .vertexSeq()) <= (G .order()) + 1 by NAT_1:12; :: thesis: verum

end;

suppose len W <> 1 ; :: thesis: len (W .vertexSeq()) <= (G .order()) + 1

then not W is trivial by Lm55;
then consider lenW2 being odd Element of NAT such that
A1: lenW2 = (len W) - 2 and
A2: (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W by Th134;
set W2 = W .cut (1,lenW2);
set vs1 = (W .cut (1,lenW2)) .vertexSeq() ;
consider f being Function such that
A3: ( dom f = (W .cut (1,lenW2)) .vertexSeq() & ( for x being set st x in (W .cut (1,lenW2)) .vertexSeq() holds
f . x = x `2 ) ) from FUNCT_1:sch 3();
A4: lenW2 < (len W) - 0 by A1, XREAL_1:15;
then A5: len (W .cut (1,lenW2)) = lenW2 by Lm22;

now

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f . x1 = f . x2 ; :: thesis: x1 = x2
consider a1, b1 being set such that
A9: x1 = [a1,b1] by A3, A6, RELAT_1:def 1;
A10: b1 = ((W .cut (1,lenW2)) .vertexSeq()) . a1 by A3, A6, A9, FUNCT_1:1;
A11: f . x1 = x1 `2 by A3, A6
.= b1 by A9, MCART_1:def 2 ;
consider a2, b2 being set such that
A12: x2 = [a2,b2] by A3, A7, RELAT_1:def 1;
A13: a2 in dom ((W .cut (1,lenW2)) .vertexSeq()) by A3, A7, A12, FUNCT_1:1;
A14: a1 in dom ((W .cut (1,lenW2)) .vertexSeq()) by A3, A6, A9, FUNCT_1:1;
A15: b2 = ((W .cut (1,lenW2)) .vertexSeq()) . a2 by A3, A7, A12, FUNCT_1:1;
A16: f . x2 = x2 `2 by A3, A7
.= b2 by A12, MCART_1:def 2 ;
reconsider a1 = a1, a2 = a2 as Element of NAT by A14, A13;

A17: now

let n1, n2 be Element of NAT ; :: thesis: ( n1 < n2 & n1 in dom ((W .cut (1,lenW2)) .vertexSeq()) & n2 in dom ((W .cut (1,lenW2)) .vertexSeq()) implies not ((W .cut (1,lenW2)) .vertexSeq()) . n1 = ((W .cut (1,lenW2)) .vertexSeq()) . n2 )
assume that
A18: n1 < n2 and
A19: n1 in dom ((W .cut (1,lenW2)) .vertexSeq()) and
A20: n2 in dom ((W .cut (1,lenW2)) .vertexSeq()) and
A21: ((W .cut (1,lenW2)) .vertexSeq()) . n1 = ((W .cut (1,lenW2)) .vertexSeq()) . n2 ; :: thesis: contradiction
A22: (2 * n2) - 1 in dom (W .cut (1,lenW2)) by A20, Th74;
A23: (2 * n1) - 1 in dom (W .cut (1,lenW2)) by A19, Th74;
then reconsider a = (2 * n1) - 1, b = (2 * n2) - 1 as odd Element of NAT by A22;
A24: (W .cut (1,lenW2)) . b = W . b by A4, A22, Lm23;
A25: n2 <= len ((W .cut (1,lenW2)) .vertexSeq()) by A20, FINSEQ_3:25;
1 <= n2 by A20, FINSEQ_3:25;
then A26: ((W .cut (1,lenW2)) .vertexSeq()) . n2 = (W .cut (1,lenW2)) . b by A25, Def14;
A27: n1 <= len ((W .cut (1,lenW2)) .vertexSeq()) by A19, FINSEQ_3:25;
1 <= n1 by A19, FINSEQ_3:25;
then A28: ((W .cut (1,lenW2)) .vertexSeq()) . n1 = (W .cut (1,lenW2)) . a by A27, Def14;
b <= lenW2 by A5, A22, FINSEQ_3:25;
then A29: b < len W by A4, XXREAL_0:2;
2 * n1 < 2 * n2 by A18, XREAL_1:68;
then A30: a < b by XREAL_1:14;
(W .cut (1,lenW2)) . a = W . a by A4, A23, Lm23;
hence contradiction by A21, A28, A26, A24, A30, A29, Def28; :: thesis: verum

end;

now

assume A31: a1 <> a2 ; :: thesis: contradiction

now

per cases ( a1 <= a2 or a1 > a2 ) ;

suppose a1 <= a2 ; :: thesis: contradiction

then a1 < a2 by A31, XXREAL_0:1;
hence contradiction by A8, A11, A16, A14, A10, A13, A15, A17; :: thesis: verum

end;

suppose a1 > a2 ; :: thesis: contradiction

hence contradiction by A8, A11, A16, A14, A10, A13, A15, A17; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence x1 = x2 by A8, A9, A12, A11, A16; :: thesis: verum

end;

then A32: f is one-to-one by FUNCT_1:def 4;

now

let y be set ; :: thesis: ( y in rng f implies y in the_Vertices_of G )
assume y in rng f ; :: thesis: y in the_Vertices_of G
then consider x being set such that
A33: x in dom f and
A34: f . x = y by FUNCT_1:def 3;
consider a, b being set such that
A35: x = [a,b] by A3, A33, RELAT_1:def 1;
y = x `2 by A3, A33, A34;
then A36: y = b by A35, MCART_1:def 2;
A37: b = ((W .cut (1,lenW2)) .vertexSeq()) . a by A3, A33, A35, FUNCT_1:1;
a in dom ((W .cut (1,lenW2)) .vertexSeq()) by A3, A33, A35, FUNCT_1:1;
then y in rng ((W .cut (1,lenW2)) .vertexSeq()) by A36, A37, FUNCT_1:def 3;
hence y in the_Vertices_of G ; :: thesis: verum

end;

then rng f c= the_Vertices_of G by TARSKI:def 3;
then card ((W .cut (1,lenW2)) .vertexSeq()) c= card (the_Vertices_of G) by A3, A32, CARD_1:10;
then card ((W .cut (1,lenW2)) .vertexSeq()) <= card (the_Vertices_of G) by NAT_1:39;
then len ((W .cut (1,lenW2)) .vertexSeq()) <= G .order() by GLIB_000:def 24;
then A38: (len ((W .cut (1,lenW2)) .vertexSeq())) + 1 <= (G .order()) + 1 by XREAL_1:7;
A39: lenW2 < (len W) - 0 by A1, XREAL_1:15;
then A40: W . (lenW2 + 1) Joins W . lenW2,W . (lenW2 + 2),G by Def3;
1 <= lenW2 by ABIAN:12;
then (W .cut (1,lenW2)) .last() = W . lenW2 by A39, Lm16, JORDAN12:2;
then W .vertexSeq() = ((W .cut (1,lenW2)) .vertexSeq()) ^ <*(W . (lenW2 + 2))*> by A2, A40, Th76;
then len (W .vertexSeq()) = (len ((W .cut (1,lenW2)) .vertexSeq())) + (len <*(W . (lenW2 + 2))*>) by FINSEQ_1:22;
hence len (W .vertexSeq()) <= (G .order()) + 1 by A38, FINSEQ_1:39; :: thesis: verum

end;

end;

end;

hence len (W .vertexSeq()) <= (G .order()) + 1 ; :: thesis: verum