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;

now :: thesis: for x being Nat st x in dom (G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)))) holds
(G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)))) . x = (W .cut (n,(n + 2))) . x

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:25;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:5;
x <= 3 by A7, A9, FINSEQ_3:25;
then A10: xaa1 < 3 - 0 by XREAL_1:15;
xaa1 + 1 = x ;
then A11: (W .cut (n,(n + 2))) . x = W . (n + xaa1) by A3, A2, A4, A10, Lm15;

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

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; :: 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; :: 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; :: 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:9; :: thesis: verum