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

for n being Element of NAT st n in dom (W .reverse()) holds

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

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

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

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

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

hence (W .reverse()) . n = W . (((len W) - n) + 1) by FINSEQ_5:def 3; :: thesis: ((len W) - n) + 1 in dom W

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

then n in Seg (len W) by FINSEQ_5:def 3;

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

hence ((len W) - n) + 1 in dom W by FINSEQ_1:def 3; :: thesis: verum

for n being Element of NAT st n in dom (W .reverse()) holds

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

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

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

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

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

hence (W .reverse()) . n = W . (((len W) - n) + 1) by FINSEQ_5:def 3; :: thesis: ((len W) - n) + 1 in dom W

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

then n in Seg (len W) by FINSEQ_5:def 3;

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

hence ((len W) - n) + 1 in dom W by FINSEQ_1:def 3; :: thesis: verum