let G be finite _Graph; :: thesis: for W being Path of G holds len () <= () + 1
let W be Path of G; :: thesis: len () <= () + 1
now :: thesis: len () <= () + 1
per cases ( len W = 1 or len W <> 1 ) ;
suppose len W = 1 ; :: thesis: len () <= () + 1
then 1 + 1 = 2 * (len ()) by Def14;
hence len () <= () + 1 by NAT_1:12; :: thesis: verum
end;
suppose len W <> 1 ; :: thesis: len () <= () + 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 Th131;
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 object st x in (W .cut (1,lenW2)) .vertexSeq() holds
f . x = x `2 ) ) from A4: lenW2 < (len W) - 0 by ;
then A5: len (W .cut (1,lenW2)) = lenW2 by Lm22;
now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: 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 object such that
A9: x1 = [a1,b1] by ;
A10: b1 = ((W .cut (1,lenW2)) .vertexSeq()) . a1 by ;
A11: f . x1 = x1 `2 by A3, A6
.= b1 by A9 ;
consider a2, b2 being object such that
A12: x2 = [a2,b2] by ;
A13: a2 in dom ((W .cut (1,lenW2)) .vertexSeq()) by ;
A14: a1 in dom ((W .cut (1,lenW2)) .vertexSeq()) by ;
A15: b2 = ((W .cut (1,lenW2)) .vertexSeq()) . a2 by ;
A16: f . x2 = x2 `2 by A3, A7
.= b2 by A12 ;
reconsider a1 = a1, a2 = a2 as Element of NAT by ;
A17: now :: thesis: for n1, n2 being Element of NAT st n1 < n2 & n1 in dom ((W .cut (1,lenW2)) .vertexSeq()) & n2 in dom ((W .cut (1,lenW2)) .vertexSeq()) holds
not ((W .cut (1,lenW2)) .vertexSeq()) . n1 = ((W .cut (1,lenW2)) .vertexSeq()) . n2
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 ;
A23: (2 * n1) - 1 in dom (W .cut (1,lenW2)) by ;
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 ;
A25: n2 <= len ((W .cut (1,lenW2)) .vertexSeq()) by ;
1 <= n2 by ;
then A26: ((W .cut (1,lenW2)) .vertexSeq()) . n2 = (W .cut (1,lenW2)) . b by ;
A27: n1 <= len ((W .cut (1,lenW2)) .vertexSeq()) by ;
1 <= n1 by ;
then A28: ((W .cut (1,lenW2)) .vertexSeq()) . n1 = (W .cut (1,lenW2)) . a by ;
b <= lenW2 by ;
then A29: b < len W by ;
2 * n1 < 2 * n2 by ;
then A30: a < b by XREAL_1:14;
(W .cut (1,lenW2)) . a = W . a by ;
hence contradiction by A21, A28, A26, A24, A30, A29, Def28; :: thesis: verum
end;
now :: thesis: not a1 <> a2
assume A31: a1 <> a2 ; :: thesis: contradiction
per cases ( a1 <= a2 or a1 > a2 ) ;
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 :: thesis: for y being object st y in rng f holds
y in the_Vertices_of G
let y be object ; :: thesis: ( y in rng f implies y in the_Vertices_of G )
assume y in rng f ; :: thesis:
then consider x being object such that
A33: x in dom f and
A34: f . x = y by FUNCT_1:def 3;
consider a, b being object such that
A35: x = [a,b] by ;
y = x `2 by A3, A33, A34;
then A36: y = b by A35;
A37: b = ((W .cut (1,lenW2)) .vertexSeq()) . a by ;
a in dom ((W .cut (1,lenW2)) .vertexSeq()) by ;
then y in rng ((W .cut (1,lenW2)) .vertexSeq()) by ;
hence y in the_Vertices_of G ; :: thesis: verum
end;
then rng f c= the_Vertices_of G by TARSKI:def 3;
then Segm (card ((W .cut (1,lenW2)) .vertexSeq())) c= Segm () by ;
then card ((W .cut (1,lenW2)) .vertexSeq()) <= card () 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 <= () + 1 by XREAL_1:7;
A39: lenW2 < (len W) - 0 by ;
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 ;
then W .vertexSeq() = ((W .cut (1,lenW2)) .vertexSeq()) ^ <*(W . (lenW2 + 2))*> by ;
then len () = (len ((W .cut (1,lenW2)) .vertexSeq())) + (len <*(W . (lenW2 + 2))*>) by FINSEQ_1:22;
hence len () <= () + 1 by ; :: thesis: verum
end;
end;
end;
hence len () <= () + 1 ; :: thesis: verum