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 ;
then A6: len (W .addEdge e) = (len W) + 2 by Lm37;
A7: (W .addEdge e) . ((len W) + 1) = e by ;
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 = () . ((W .addEdge e) . (n + 1))
let n be odd Element of NAT ; :: thesis: ( n < len (W .addEdge e) implies (W .addEdge e) . n = () . ((W .addEdge e) . (n + 1)) )
assume n < len (W .addEdge e) ; :: thesis: (W .addEdge e) . n = () . ((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 = () . ((W .addEdge e) . (n + 1))
per cases ( n = len W or n <> len W ) ;
suppose n = len W ; :: thesis: (W .addEdge e) . n = () . ((W .addEdge e) . (n + 1))
hence (W .addEdge e) . n = () . ((W .addEdge e) . (n + 1)) by ; :: thesis: verum
end;
suppose A10: n <> len W ; :: thesis: (W .addEdge e) . n = () . ((W .addEdge e) . (n + 1))
A11: 1 <= n + 1 by NAT_1:12;
1 <= n by ABIAN:12;
then n in dom W by ;
then A12: (W .addEdge e) . n = W . n by ;
A13: n < len W by ;
then n + 1 <= len W by NAT_1:13;
then n + 1 in dom W by ;
then (W .addEdge e) . (n + 1) = W . (n + 1) by ;
hence (W .addEdge e) . n = () . ((W .addEdge e) . (n + 1)) by A1, A13, A12; :: thesis: verum
end;
end;
end;
hence (W .addEdge e) . n = () . ((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