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() )
assume A1: 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 A2: ( W is_Walk_from x,y & ( for W2 being DPath of G st W2 is_Walk_from x,y holds
W .cost() <= W2 .cost() ) ) by Def2;
set WC = W .cut m,n;
A3: W .cut m,n is_Walk_from (W .cut m,n) .first() ,(W .cut m,n) .last() by GLIB_001:def 23;
A4: ( W . 1 = x & W . (len W) = y ) by A2, GLIB_001:18;

now

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

suppose A5: ( not m is even & not n is even & 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: ( not 1 is even & 1 <= m & 1 <= n ) by A5, HEYTING3:1, JORDAN12:3;
then A7: (W .cut 1,m) .append (W .cut m,n) = W .cut 1,n by A5, GLIB_001:39;
A8: (W .cut 1,n) .append (W .cut n,(len W)) = W .cut 1,(len W) by A5, A6, GLIB_001:39
.= W by GLIB_001:40 ;
(W .cut 1,n) .last() = W . n by A5, A6, GLIB_001:38
.= (W .cut n,(len W)) .first() by A5, GLIB_001:38 ;
then A9: W .cost() = ((W .cut 1,n) .cost() ) + ((W .cut n,(len W)) .cost() ) by A8, GLIB_003:31;
A10: m <= len W by A5, XXREAL_0:2;
then (W .cut 1,m) .last() = W . m by A5, A6, GLIB_001:38
.= (W .cut m,n) .first() by A5, GLIB_001:38 ;
then (W .cut 1,n) .cost() = ((W .cut 1,m) .cost() ) + ((W .cut m,n) .cost() ) by A7, GLIB_003:31;
then A11: W .cost() = ((W .cut m,n) .cost() ) + (((W .cut 1,m) .cost() ) + ((W .cut n,(len W)) .cost() )) by A9;
A12: W .cut 1,m is_Walk_from W . 1,W . m by A5, A6, A10, GLIB_001:38;
A13: W .cut n,(len W) is_Walk_from W . n,W . (len W) by A5, GLIB_001:38;

now

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
A14: ( W2 is_Walk_from (W .cut m,n) .first() ,(W .cut m,n) .last() & W2 .cost() < (W .cut m,n) .cost() ) by A3, Def2;
A15: ( (W .cut m,n) .first() = W . m & (W .cut m,n) .last() = W . n ) by A5, GLIB_001:38;
then A16: ( W2 .first() = W . m & W2 .last() = W . n ) by A14, GLIB_001:def 23;
set WA = (W .cut 1,m) .append W2;
set WB = ((W .cut 1,m) .append W2) .append (W .cut n,(len W));
(W .cut 1,m) .append W2 is_Walk_from W . 1,W . n by A12, A14, A15, GLIB_001:32;
then A17: ((W .cut 1,m) .append W2) .append (W .cut n,(len W)) is_Walk_from x,y by A4, A13, GLIB_001:32;
A18: (W .cut 1,m) .last() = W2 .first() by A5, A6, A10, A16, GLIB_001:38;
then A19: ((W .cut 1,m) .append W2) .cost() = ((W .cut 1,m) .cost() ) + (W2 .cost() ) by GLIB_003:31;
(W .cut n,(len W)) .first() = W2 .last() by A5, A16, GLIB_001:38
.= ((W .cut 1,m) .append W2) .last() by A18, GLIB_001:31 ;
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 A19, GLIB_003:31
.= (W2 .cost() ) + (((W .cut 1,m) .cost() ) + ((W .cut n,(len W)) .cost() )) ;
then A20: (((W .cut 1,m) .append W2) .append (W .cut n,(len W))) .cost() < W .cost() by A11, A14, XREAL_1:10;
consider WB2 being DPath of ((W .cut 1,m) .append W2) .append (W .cut n,(len W));
WB2 .cost() <= (((W .cut 1,m) .append W2) .append (W .cut n,(len W))) .cost() by GLIB_003:37;
then A21: WB2 .cost() < W .cost() by A20, XXREAL_0:2;
WB2 is_Walk_from x,y by A17, GLIB_001:161;
hence contradiction by A1, A21, Def2; :: 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 A22: ( m is even or n is even 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 W .cut m,n = W by GLIB_001:def 11;
then ( (W .cut m,n) .first() = x & (W .cut m,n) .last() = y ) by A2, GLIB_001:def 23;
hence W .cut m,n is_mincost_DPath_from (W .cut m,n) .first() ,(W .cut m,n) .last() by A1, A22, GLIB_001:def 11; :: 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