let G be _finite nonnegative-weighted WGraph; :: thesis: for W being DPath of G
for x, y being set
for m, n being Element of NAT st W is_mincost_DPath_from x,y holds
W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
let W be DPath of G; :: thesis: for x, y being set
for m, n being Element of NAT st W is_mincost_DPath_from x,y holds
W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
let x, y be set ; :: thesis: for m, n being Element of NAT st W is_mincost_DPath_from x,y holds
W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
let m, n be Element of NAT ; :: thesis: ( W is_mincost_DPath_from x,y implies W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() )
set WC = W .cut (m,n);
A1: W .cut (m,n) is_Walk_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() by GLIB_001:def 23;
assume A2: W is_mincost_DPath_from x,y ; :: thesis: W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
then A3: W is_Walk_from x,y ;
then A4: ( W . 1 = x & W . (len W) = y ) by GLIB_001:17;

now :: thesis: W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()

per cases ( ( m is odd & n is odd & m <= n & n <= len W ) or not m is odd or not n is odd or not m <= n or not n <= len W ) ;

suppose A5: ( m is odd & n is odd & m <= n & n <= len W ) ; :: thesis: W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()

set W1 = W .cut (1,m);
set W3 = W .cut (n,(len W));
A6: 1 <= n by A5, ABIAN:12;
then A7: (W .cut (1,n)) .append (W .cut (n,(len W))) = W .cut (1,(len W)) by A5, GLIB_001:38, JORDAN12:2
.= W by GLIB_001:39 ;
(W .cut (1,n)) .last() = W . n by A5, A6, GLIB_001:37, JORDAN12:2
.= (W .cut (n,(len W))) .first() by A5, GLIB_001:37 ;
then A8: W .cost() = ((W .cut (1,n)) .cost()) + ((W .cut (n,(len W))) .cost()) by A7, GLIB_003:24;
A9: 1 <= m by A5, ABIAN:12;
then A10: (W .cut (1,m)) .append (W .cut (m,n)) = W .cut (1,n) by A5, GLIB_001:38, JORDAN12:2;
A11: m <= len W by A5, XXREAL_0:2;
then (W .cut (1,m)) .last() = W . m by A5, A9, GLIB_001:37, JORDAN12:2
.= (W .cut (m,n)) .first() by A5, GLIB_001:37 ;
then (W .cut (1,n)) .cost() = ((W .cut (1,m)) .cost()) + ((W .cut (m,n)) .cost()) by A10, GLIB_003:24;
then A12: W .cost() = ((W .cut (m,n)) .cost()) + (((W .cut (1,m)) .cost()) + ((W .cut (n,(len W))) .cost())) by A8;
A13: W .cut (n,(len W)) is_Walk_from W . n,W . (len W) by A5, GLIB_001:37;
A14: W .cut (1,m) is_Walk_from W . 1,W . m by A5, A9, A11, GLIB_001:37, JORDAN12:2;

now :: thesis: W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()

assume not W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() ; :: thesis: contradiction
then consider W2 being DPath of G such that
A15: W2 is_Walk_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() and
A16: W2 .cost() < (W .cut (m,n)) .cost() by A1;
set WA = (W .cut (1,m)) .append W2;
set WB = ((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)));
set WB2 = the DPath of ((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)));
A17: (W .cut (m,n)) .last() = W . n by A5, GLIB_001:37;
A18: (W .cut (m,n)) .first() = W . m by A5, GLIB_001:37;
then (W .cut (1,m)) .append W2 is_Walk_from W . 1,W . n by A14, A15, A17, GLIB_001:31;
then ((W .cut (1,m)) .append W2) .append (W .cut (n,(len W))) is_Walk_from x,y by A4, A13, GLIB_001:31;
then A19: the DPath of ((W .cut (1,m)) .append W2) .append (W .cut (n,(len W))) is_Walk_from x,y by GLIB_001:160;
W2 .first() = W . m by A15, A18, GLIB_001:def 23;
then A20: (W .cut (1,m)) .last() = W2 .first() by A5, A9, A11, GLIB_001:37, JORDAN12:2;
then A21: ((W .cut (1,m)) .append W2) .cost() = ((W .cut (1,m)) .cost()) + (W2 .cost()) by GLIB_003:24;
W2 .last() = W . n by A15, A17, GLIB_001:def 23;
then (W .cut (n,(len W))) .first() = W2 .last() by A5, GLIB_001:37
.= ((W .cut (1,m)) .append W2) .last() by A20, GLIB_001:30 ;
then (((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)))) .cost() = (((W .cut (1,m)) .cost()) + (W2 .cost())) + ((W .cut (n,(len W))) .cost()) by A21, GLIB_003:24
.= (W2 .cost()) + (((W .cut (1,m)) .cost()) + ((W .cut (n,(len W))) .cost())) ;
then A22: (((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)))) .cost() < W .cost() by A12, A16, XREAL_1:8;
the DPath of ((W .cut (1,m)) .append W2) .append (W .cut (n,(len W))) .cost() <= (((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)))) .cost() by GLIB_003:30;
then the DPath of ((W .cut (1,m)) .append W2) .append (W .cut (n,(len W))) .cost() < W .cost() by A22, XXREAL_0:2;
hence contradiction by A2, A19; :: thesis: verum

end;

hence W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() ; :: thesis: verum

end;

suppose ( not m is odd or not n is odd or not m <= n or not n <= len W ) ; :: thesis: W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()

then A23: W .cut (m,n) = W by GLIB_001:def 11;
then (W .cut (m,n)) .first() = x by A3, GLIB_001:def 23;
hence W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() by A2, A23, GLIB_001:def 23; :: thesis: verum

end;

end;

end;

hence W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() ; :: thesis: verum