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;

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))

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;

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

per cases ( n = len W or n <> len W ) ;

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;

end;

end;

hence (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1)) ; :: thesis: verum

end;

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