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

for x, e, y, z being set st W is directed & W is_Walk_from x,y & e DJoins y,z,G holds

( W .addEdge e is directed & W .addEdge e is_Walk_from x,z )

let W be Walk of G; :: thesis: for x, e, y, z being set st W is directed & W is_Walk_from x,y & e DJoins y,z,G holds

( W .addEdge e is directed & W .addEdge e is_Walk_from x,z )

let x, e, y, z be set ; :: thesis: ( W is directed & W is_Walk_from x,y & e DJoins y,z,G implies ( W .addEdge e is directed & W .addEdge e is_Walk_from x,z ) )

set W2 = W .addEdge e;

assume that

A1: W is directed and

A2: W is_Walk_from x,y and

A3: e DJoins y,z,G ; :: thesis: ( W .addEdge e is directed & W .addEdge e is_Walk_from x,z )

A4: W .last() = y by A2;

then A5: e Joins W .last() ,z,G by A3, GLIB_000:16;

then A6: len (W .addEdge e) = (len W) + 2 by Lm37;

A7: (W .addEdge e) . ((len W) + 1) = e by A5, Lm38;

1 <= len W by ABIAN:12;

then len W in dom W by FINSEQ_3:25;

then A8: (W .addEdge e) . (len W) = y by A4, A5, Lm38;

thus W .addEdge e is_Walk_from x,z by A2, A5, Lm39; :: thesis: verum

for x, e, y, z being set st W is directed & W is_Walk_from x,y & e DJoins y,z,G holds

( W .addEdge e is directed & W .addEdge e is_Walk_from x,z )

let W be Walk of G; :: thesis: for x, e, y, z being set st W is directed & W is_Walk_from x,y & e DJoins y,z,G holds

( W .addEdge e is directed & W .addEdge e is_Walk_from x,z )

let x, e, y, z be set ; :: thesis: ( W is directed & W is_Walk_from x,y & e DJoins y,z,G implies ( W .addEdge e is directed & W .addEdge e is_Walk_from x,z ) )

set W2 = W .addEdge e;

assume that

A1: W is directed and

A2: W is_Walk_from x,y and

A3: e DJoins y,z,G ; :: thesis: ( W .addEdge e is directed & W .addEdge e is_Walk_from x,z )

A4: W .last() = y by A2;

then A5: e Joins W .last() ,z,G by A3, GLIB_000:16;

then A6: len (W .addEdge e) = (len W) + 2 by Lm37;

A7: (W .addEdge e) . ((len W) + 1) = e by A5, Lm38;

1 <= len W by ABIAN:12;

then len W in dom W by FINSEQ_3:25;

then A8: (W .addEdge e) . (len W) = y by A4, A5, Lm38;

now :: thesis: for n being odd Element of NAT st n < len (W .addEdge e) holds

(W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1))

hence
W .addEdge e is directed
; :: thesis: W .addEdge e is_Walk_from x,z(W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1))

let n be odd Element of NAT ; :: thesis: ( n < len (W .addEdge e) implies (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1)) )

assume n < len (W .addEdge e) ; :: thesis: (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1))

then n < ((len W) + 1) + 1 by A6;

then n <= (len W) + 1 by NAT_1:13;

then n < (len W) + 1 by XXREAL_0:1;

then A9: n <= len W by NAT_1:13;

end;assume n < len (W .addEdge e) ; :: thesis: (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1))

then n < ((len W) + 1) + 1 by A6;

then n <= (len W) + 1 by NAT_1:13;

then n < (len W) + 1 by XXREAL_0:1;

then A9: n <= len W by NAT_1:13;

now :: thesis: (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1))end;

hence
(W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1))
; :: thesis: verumper cases
( n = len W or n <> len W )
;

end;

suppose
n = len W
; :: thesis: (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1))

hence
(W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1))
by A3, A8, A7, GLIB_000:def 14; :: thesis: verum

end;suppose A10:
n <> len W
; :: thesis: (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1))

A11:
1 <= n + 1
by NAT_1:12;

1 <= n by ABIAN:12;

then n in dom W by A9, FINSEQ_3:25;

then A12: (W .addEdge e) . n = W . n by A5, Lm38;

A13: n < len W by A9, A10, XXREAL_0:1;

then n + 1 <= len W by NAT_1:13;

then n + 1 in dom W by A11, FINSEQ_3:25;

then (W .addEdge e) . (n + 1) = W . (n + 1) by A5, Lm38;

hence (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1)) by A1, A13, A12; :: thesis: verum

end;1 <= n by ABIAN:12;

then n in dom W by A9, FINSEQ_3:25;

then A12: (W .addEdge e) . n = W . n by A5, Lm38;

A13: n < len W by A9, A10, XXREAL_0:1;

then n + 1 <= len W by NAT_1:13;

then n + 1 in dom W by A11, FINSEQ_3:25;

then (W .addEdge e) . (n + 1) = W . (n + 1) by A5, Lm38;

hence (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1)) by A1, A13, A12; :: thesis: verum

thus W .addEdge e is_Walk_from x,z by A2, A5, Lm39; :: thesis: verum