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 not W is trivial by Lm55;
then consider lenW2 being odd Element of NAT such that
A1: ( lenW2 = (len W) - 2 & (W .cut 1,lenW2) .addEdge (W . (lenW2 + 1)) = W ) by Th134;
set W2 = W .cut 1,lenW2;
set vs1 = (W .cut 1,lenW2) .vertexSeq() ;
A2: lenW2 < (len W) - 0 by A1, XREAL_1:17;
then A3: len (W .cut 1,lenW2) = lenW2 by Lm22;
consider f being Function such that
A4: ( 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();
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
A5: ( x in dom f & f . x = y ) by FUNCT_1:def 5;
consider a, b being set such that
A6: x = [a,b] by A4, A5, RELAT_1:def 1;
y = x `2 by A4, A5;
then A7: y = b by A6, MCART_1:def 2;
( a in dom ((W .cut 1,lenW2) .vertexSeq() ) & b = ((W .cut 1,lenW2) .vertexSeq() ) . a ) by A4, A5, A6, FUNCT_1:8;
then y in rng ((W .cut 1,lenW2) .vertexSeq() ) by A7, FUNCT_1:def 5;
hence y in the_Vertices_of G ; :: thesis: verum
end;
then A8: rng f c= the_Vertices_of G by TARSKI:def 3;
now
let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A9: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then consider a1, b1 being set such that
A10: x1 = [a1,b1] by A4, RELAT_1:def 1;
consider a2, b2 being set such that
A11: x2 = [a2,b2] by A4, A9, RELAT_1:def 1;
A12: f . x1 = x1 `2 by A4, A9
.= b1 by A10, MCART_1:def 2 ;
A13: f . x2 = x2 `2 by A4, A9
.= b2 by A11, MCART_1:def 2 ;
A14: ( a1 in dom ((W .cut 1,lenW2) .vertexSeq() ) & b1 = ((W .cut 1,lenW2) .vertexSeq() ) . a1 & a2 in dom ((W .cut 1,lenW2) .vertexSeq() ) & b2 = ((W .cut 1,lenW2) .vertexSeq() ) . a2 ) by A4, A9, A10, A11, FUNCT_1:8;
then reconsider a1 = a1, a2 = a2 as Element of NAT ;
A15: 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 A16: ( n1 < n2 & n1 in dom ((W .cut 1,lenW2) .vertexSeq() ) & n2 in dom ((W .cut 1,lenW2) .vertexSeq() ) & ((W .cut 1,lenW2) .vertexSeq() ) . n1 = ((W .cut 1,lenW2) .vertexSeq() ) . n2 ) ; :: thesis: contradiction
then A17: ( (2 * n1) - 1 in dom (W .cut 1,lenW2) & (2 * n2) - 1 in dom (W .cut 1,lenW2) ) by Th74;
then reconsider a = (2 * n1) - 1, b = (2 * n2) - 1 as odd Element of NAT ;
( 1 <= n1 & n1 <= len ((W .cut 1,lenW2) .vertexSeq() ) & 1 <= n2 & n2 <= len ((W .cut 1,lenW2) .vertexSeq() ) ) by A16, FINSEQ_3:27;
then A18: ( ((W .cut 1,lenW2) .vertexSeq() ) . n1 = (W .cut 1,lenW2) . a & ((W .cut 1,lenW2) .vertexSeq() ) . n2 = (W .cut 1,lenW2) . b ) by Def14;
A19: ( (W .cut 1,lenW2) . a = W . a & (W .cut 1,lenW2) . b = W . b ) by A2, A17, Lm23;
2 * n1 < 2 * n2 by A16, XREAL_1:70;
then A20: a < b by XREAL_1:16;
b <= lenW2 by A3, A17, FINSEQ_3:27;
then b < len W by A2, XXREAL_0:2;
hence contradiction by A16, A18, A19, A20, Def28; :: thesis: verum
end;
now
assume A21: a1 <> a2 ; :: thesis: contradiction
hence contradiction ; :: thesis: verum
end;
hence x1 = x2 by A9, A10, A11, A12, A13; :: thesis: verum
end;
then f is one-to-one by FUNCT_1:def 8;
then card ((W .cut 1,lenW2) .vertexSeq() ) c= card (the_Vertices_of G) by A4, A8, CARD_1:26;
then card ((W .cut 1,lenW2) .vertexSeq() ) <= card (the_Vertices_of G) by NAT_1:40;
then len ((W .cut 1,lenW2) .vertexSeq() ) <= G .order() by GLIB_000:def 26;
then A22: (len ((W .cut 1,lenW2) .vertexSeq() )) + 1 <= (G .order() ) + 1 by XREAL_1:9;
A23: lenW2 < (len W) - 0 by A1, XREAL_1:17;
then A24: W . (lenW2 + 1) Joins W . lenW2,W . (lenW2 + 2),G by Def3;
( not 1 is even & 1 <= lenW2 ) by HEYTING3:1, JORDAN12:3;
then (W .cut 1,lenW2) .last() = W . lenW2 by A23, Lm16;
then W .vertexSeq() = ((W .cut 1,lenW2) .vertexSeq() ) ^ <*(W . (lenW2 + 2))*> by A1, A24, Th76;
then len (W .vertexSeq() ) = (len ((W .cut 1,lenW2) .vertexSeq() )) + (len <*(W . (lenW2 + 2))*>) by FINSEQ_1:35;
hence len (W .vertexSeq() ) <= (G .order() ) + 1 by A22, FINSEQ_1:56; :: thesis: verum
end;
end;
end;
hence len (W .vertexSeq() ) <= (G .order() ) + 1 ; :: thesis: verum