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;

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

hence
G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = W .cut (n,(n + 2))
by A4, A7, FINSEQ_2:9; :: thesis: verum(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;

end;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))) . xend;

hence
(G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2)))) . x = (W .cut (n,(n + 2))) . x
; :: thesis: verumper cases
( x = 1 or x = 2 or x = 3 )
by A8, A9, ENUMSET1:def 1, FINSEQ_3:1;

end;

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

end;