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, Th15;
then A8: dom (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) = Seg 3 by FINSEQ_1:def 3;

now

let x be Nat; :: thesis: ( x in dom (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) implies (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) . x = (W .cut n,(n + 2)) . x )
assume A9: x in dom (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) ; :: thesis: (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) . x = (W .cut n,(n + 2)) . x
then 1 <= x by FINSEQ_3:27;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:18;
x <= 3 by A7, A9, FINSEQ_3:27;
then A10: xaa1 < 3 - 0 by XREAL_1:17;
xaa1 + 1 = x ;
then A11: (W .cut n,(n + 2)) . x = W . (n + xaa1) by A3, A2, A4, A10, Lm15;

now

per cases ( x = 1 or x = 2 or x = 3 ) by A8, A9, ENUMSET1:def 1, FINSEQ_3:1;

suppose x = 1 ; :: thesis: (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) . x = (W .cut n,(n + 2)) . x

hence (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) . x = (W .cut n,(n + 2)) . x by A6, A11, FINSEQ_1:62; :: thesis: verum

end;

suppose x = 2 ; :: thesis: (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) . x = (W .cut n,(n + 2)) . x

hence (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) . x = (W .cut n,(n + 2)) . x by A6, A11, FINSEQ_1:62; :: thesis: verum

end;

suppose x = 3 ; :: thesis: (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) . x = (W .cut n,(n + 2)) . x

hence (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) . x = (W .cut n,(n + 2)) . x by A6, A11, FINSEQ_1:62; :: thesis: verum

end;

end;

end;

hence (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) . x = (W .cut n,(n + 2)) . x ; :: thesis: verum

end;

hence G .walkOf (W . n),(W . (n + 1)),(W . (n + 2)) = W .cut n,(n + 2) by A4, A7, FINSEQ_2:10; :: thesis: verum