let G be _Graph; :: thesis: for W being Walk of G

for n being Element of NAT st n in dom W holds

( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) )

let W be Walk of G; :: thesis: for n being Element of NAT st n in dom W holds

( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) )

let n be Element of NAT ; :: thesis: ( n in dom W implies ( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) ) )

set rn = ((len W) - n) + 1;

assume A1: n in dom W ; :: thesis: ( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) )

then n <= len W by FINSEQ_3:25;

then reconsider rn = ((len W) - n) + 1 as Element of NAT by FINSEQ_5:1;

n in Seg (len W) by A1, FINSEQ_1:def 3;

then ((len W) - n) + 1 in Seg (len W) by FINSEQ_5:2;

then A2: rn in Seg (len (W .reverse())) by FINSEQ_5:def 3;

then rn in dom (W .reverse()) by FINSEQ_1:def 3;

then (W .reverse()) . rn = W . (((len W) - rn) + 1) by FINSEQ_5:def 3;

hence ( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) ) by A2, FINSEQ_1:def 3; :: thesis: verum

for n being Element of NAT st n in dom W holds

( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) )

let W be Walk of G; :: thesis: for n being Element of NAT st n in dom W holds

( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) )

let n be Element of NAT ; :: thesis: ( n in dom W implies ( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) ) )

set rn = ((len W) - n) + 1;

assume A1: n in dom W ; :: thesis: ( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) )

then n <= len W by FINSEQ_3:25;

then reconsider rn = ((len W) - n) + 1 as Element of NAT by FINSEQ_5:1;

n in Seg (len W) by A1, FINSEQ_1:def 3;

then ((len W) - n) + 1 in Seg (len W) by FINSEQ_5:2;

then A2: rn in Seg (len (W .reverse())) by FINSEQ_5:def 3;

then rn in dom (W .reverse()) by FINSEQ_1:def 3;

then (W .reverse()) . rn = W . (((len W) - rn) + 1) by FINSEQ_5:def 3;

hence ( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) ) by A2, FINSEQ_1:def 3; :: thesis: verum