let G be _Graph; :: thesis: for W being Walk of G

for m, n being Element of NAT st W is directed holds

W .cut (m,n) is directed

let W be Walk of G; :: thesis: for m, n being Element of NAT st W is directed holds

W .cut (m,n) is directed

let m, n be Element of NAT ; :: thesis: ( W is directed implies W .cut (m,n) is directed )

set W2 = W .cut (m,n);

assume A1: W is directed ; :: thesis: W .cut (m,n) is directed

for m, n being Element of NAT st W is directed holds

W .cut (m,n) is directed

let W be Walk of G; :: thesis: for m, n being Element of NAT st W is directed holds

W .cut (m,n) is directed

let m, n be Element of NAT ; :: thesis: ( W is directed implies W .cut (m,n) is directed )

set W2 = W .cut (m,n);

assume A1: W is directed ; :: thesis: W .cut (m,n) is directed

now :: thesis: W .cut (m,n) is directed end;

hence
W .cut (m,n) is directed
; :: thesis: verumper 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 )
;

end;

suppose A2:
( m is odd & n is odd & m <= n & n <= len W )
; :: thesis: W .cut (m,n) is directed

then reconsider m9 = m as odd Element of NAT ;

end;now :: thesis: for x being odd Element of NAT st x < len (W .cut (m,n)) holds

(W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G

hence
W .cut (m,n) is directed
by Lm51; :: thesis: verum(W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G

let x be odd Element of NAT ; :: thesis: ( x < len (W .cut (m,n)) implies (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G )

reconsider xaa1 = x - 1 as even Element of NAT by ABIAN:12, INT_1:5;

assume A3: x < len (W .cut (m,n)) ; :: thesis: (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G

then x + 1 <= len (W .cut (m,n)) by NAT_1:13;

then A4: x + 1 < len (W .cut (m,n)) by XXREAL_0:1;

m + x in dom W by A2, A3, Lm15;

then m9 + x <= len W by FINSEQ_3:25;

then A5: (m9 + x) - 1 < (len W) - 0 by XREAL_1:15;

xaa1 < (len (W .cut (m,n))) - 0 by A3, XREAL_1:14;

then A6: (W .cut (m,n)) . (xaa1 + 1) = W . (m + xaa1) by A2, Lm15;

A7: (W .cut (m,n)) . (x + 2) = (W .cut (m,n)) . ((x + 1) + 1)

.= W . (m + (((x - 1) + 1) + 1)) by A2, A4, Lm15

.= W . ((m + xaa1) + 2) ;

(W .cut (m,n)) . (x + 1) = W . (((m + x) - 1) + 1) by A2, A3, Lm15

.= W . ((m + xaa1) + 1) ;

hence (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G by A1, A6, A5, A7, Lm51; :: thesis: verum

end;reconsider xaa1 = x - 1 as even Element of NAT by ABIAN:12, INT_1:5;

assume A3: x < len (W .cut (m,n)) ; :: thesis: (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G

then x + 1 <= len (W .cut (m,n)) by NAT_1:13;

then A4: x + 1 < len (W .cut (m,n)) by XXREAL_0:1;

m + x in dom W by A2, A3, Lm15;

then m9 + x <= len W by FINSEQ_3:25;

then A5: (m9 + x) - 1 < (len W) - 0 by XREAL_1:15;

xaa1 < (len (W .cut (m,n))) - 0 by A3, XREAL_1:14;

then A6: (W .cut (m,n)) . (xaa1 + 1) = W . (m + xaa1) by A2, Lm15;

A7: (W .cut (m,n)) . (x + 2) = (W .cut (m,n)) . ((x + 1) + 1)

.= W . (m + (((x - 1) + 1) + 1)) by A2, A4, Lm15

.= W . ((m + xaa1) + 2) ;

(W .cut (m,n)) . (x + 1) = W . (((m + x) - 1) + 1) by A2, A3, Lm15

.= W . ((m + xaa1) + 1) ;

hence (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G by A1, A6, A5, A7, Lm51; :: thesis: verum