let G be _Graph; 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; 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 ; ( W is directed implies W .cut (m,n) is directed )
set W2 = W .cut (m,n);
assume A1:
W is directed
; W .cut (m,n) is directed
now W .cut (m,n) is directed 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 A2:
(
m is
odd &
n is
odd &
m <= n &
n <= len W )
;
W .cut (m,n) is directed then reconsider m9 =
m as
odd Element of
NAT ;
now 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),Glet x be
odd Element of
NAT ;
( 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))
;
(W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),Gthen
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;
verum end; hence
W .cut (
m,
n) is
directed
by Lm51;
verum end;
hence
W .cut (m,n) is directed
; verum