let G be _Graph; :: thesis: for W being Walk of G
for n being odd Element of NAT st n < len W holds
G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = W .cut (n,(n + 2))
let W be Walk of G; :: thesis: for n being odd Element of NAT st n < len W holds
G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = W .cut (n,(n + 2))
let n be odd Element of NAT ; :: thesis: ( n < len W implies G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = W .cut (n,(n + 2)) )
set v1 = W . n;
set e = W . (n + 1);
set v2 = W . (n + 2);
set W1 = G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)));
set W2 = W .cut (n,(n + 2));
assume A1: n < len W ; :: thesis: G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = W .cut (n,(n + 2))
then A2: n + 2 <= len W by Th1;
A3: n <= n + 2 by Th1;
then A4: (len (W .cut (n,(n + 2)))) + n = 1 + (2 + n) by A2, Lm15;
A5: W . (n + 1) Joins W . n,W . (n + 2),G by A1, Def3;
then A6: G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = <*(W . n),(W . (n + 1)),(W . (n + 2))*> by Def5;
A7: len (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)))) = 3 by A5, Th13;
then A8: dom (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)))) = Seg 3 by FINSEQ_1:def 3;
hence G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = W .cut (n,(n + 2)) by A4, A7, FINSEQ_2:9; :: thesis: verum