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 A1: ( W is directed & W is_Walk_from x,y & e DJoins y,z,G ) ; :: thesis: ( W .addEdge e is directed & W .addEdge e is_Walk_from x,z )
then A2: W .last() = y by Def23;
then A3: e Joins W .last() ,z,G by A1, GLIB_000:19;
then A4: len (W .addEdge e) = (len W) + 2 by Lm37;
1 <= len W by HEYTING3:1;
then len W in dom W by FINSEQ_3:27;
then A5: (W .addEdge e) . (len W) = y by A2, A3, Lm38;
A6: (W .addEdge e) . ((len W) + 1) = e by A3, Lm38;

now

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 A4;
then n <= (len W) + 1 by NAT_1:13;
then n < (len W) + 1 by XXREAL_0:1;
then A7: n <= len W by NAT_1:13;

now

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 A1, A5, A6, GLIB_000:def 16; :: thesis: verum

end;

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

then A8: n < len W by A7, XXREAL_0:1;
1 <= n by HEYTING3:1;
then n in dom W by A7, FINSEQ_3:27;
then A9: (W .addEdge e) . n = W . n by A3, Lm38;
A10: 1 <= n + 1 by NAT_1:12;
n + 1 <= len W by A8, NAT_1:13;
then n + 1 in dom W by A10, FINSEQ_3:27;
then (W .addEdge e) . (n + 1) = W . (n + 1) by A3, Lm38;
hence (W .addEdge e) . n = (the_Source_of G) . ((W .addEdge e) . (n + 1)) by A1, A8, A9, Def25; :: 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 by Def25; :: thesis: W .addEdge e is_Walk_from x,z
thus W .addEdge e is_Walk_from x,z by A1, A2, A3, Lm39; :: thesis: verum