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);
assume A1: n < len W ; :: thesis: G .walkOf (W . n),(W . (n + 1)),(W . (n + 2)) = W .cut n,(n + 2)
then A2: W . (n + 1) Joins W . n,W . (n + 2),G by Def3;
then A3: G .walkOf (W . n),(W . (n + 1)),(W . (n + 2)) = <*(W . n),(W . (n + 1)),(W . (n + 2))*> by Def5;
set W1 = G .walkOf (W . n),(W . (n + 1)),(W . (n + 2));
set W2 = W .cut n,(n + 2);
A4: ( n <= n + 2 & n + 2 <= len W ) by A1, Th1;
then A5: (len (W .cut n,(n + 2))) + n = 1 + (2 + n) by Lm15;
A6: len (G .walkOf (W . n),(W . (n + 1)),(W . (n + 2))) = 3 by A2, Th15;
then X: 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 A7: 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 A8: ( 1 <= x & x <= 3 ) by A6, FINSEQ_3:27;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:18;
A9: xaa1 + 1 = x ;
xaa1 < 3 - 0 by A8, XREAL_1:17;
then A10: (W .cut n,(n + 2)) . x = W . (n + xaa1) by A4, A5, A9, Lm15;

now

per cases ( x = 1 or x = 2 or x = 3 ) by A7, X, 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 A3, A10, 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 A3, A10, 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 A3, A10, 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 A5, A6, FINSEQ_2:10; :: thesis: verum