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

let W be Path of G; :: thesis: len (W .vertexSeq()) <= (G .order()) + 1

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

hence
len (W .vertexSeq()) <= (G .order()) + 1
; :: thesis: verumper cases
( len W = 1 or len W <> 1 )
;

end;

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;hence len (W .vertexSeq()) <= (G .order()) + 1 by NAT_1:12; :: thesis: verum

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 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 FUNCT_1:sch 3();

A4: lenW2 < (len W) - 0 by A1, XREAL_1:15;

then A5: len (W .cut (1,lenW2)) = lenW2 by Lm22;

then Segm (card ((W .cut (1,lenW2)) .vertexSeq())) c= Segm (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, Th73;

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;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 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 :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

then A32:
f is one-to-one
by FUNCT_1:def 4;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 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 ;

consider a2, b2 being object 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 ;

reconsider a1 = a1, a2 = a2 as Element of NAT by A14, A13;

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

consider a2, b2 being object 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 ;

reconsider a1 = a1, a2 = a2 as Element of NAT by A14, A13;

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

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 A20, Th71;

A23: (2 * n1) - 1 in dom (W .cut (1,lenW2)) by A19, Th71;

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

A23: (2 * n1) - 1 in dom (W .cut (1,lenW2)) by A19, Th71;

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

now :: thesis: not a1 <> a2

hence
x1 = x2
by A8, A9, A12, A11, A16; :: thesis: verumassume A31:
a1 <> a2
; :: thesis: contradiction

end;now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;

now :: thesis: for y being object st y in rng f holds

y in the_Vertices_of G

then
rng f c= the_Vertices_of G
by TARSKI:def 3;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: y in the_Vertices_of G

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 A3, A33, RELAT_1:def 1;

y = x `2 by A3, A33, A34;

then A36: y = b by A35;

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;assume y in rng f ; :: thesis: y in the_Vertices_of G

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 A3, A33, RELAT_1:def 1;

y = x `2 by A3, A33, A34;

then A36: y = b by A35;

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

then Segm (card ((W .cut (1,lenW2)) .vertexSeq())) c= Segm (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, Th73;

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