let G be _Graph; :: thesis: for W being Walk of G holds () .edgeSeq() = Rev ()
let W be Walk of G; :: thesis:
set W1 = () .edgeSeq() ;
set W2 = Rev ();
A1: len W = len () by FINSEQ_5:def 3;
len W = (2 * (len ())) + 1 by Def15;
then A2: (2 * (len ())) + 1 = (2 * (len ())) + 1 by ;
A3: now :: thesis: for n being Nat st 1 <= n & n <= len () holds
() . n = (Rev ()) . n
let n be Nat; :: thesis: ( 1 <= n & n <= len () implies () . n = (Rev ()) . n )
assume that
A4: 1 <= n and
A5: n <= len () ; :: thesis: () . n = (Rev ()) . n
A6: ((W .reverse()) .edgeSeq()) . n = () . (2 * n) by ;
set rn = ((len ()) - n) + 1;
reconsider rn = ((len ()) - n) + 1 as Element of NAT by ;
A7: n in Seg (len ()) by ;
then A8: rn in Seg (len ()) by FINSEQ_5:2;
then A9: 1 <= rn by FINSEQ_1:1;
A10: n in dom () by ;
then A11: 2 * n in dom W by Lm41;
then A12: 1 <= 2 * n by FINSEQ_3:25;
A13: rn <= len () by ;
A14: ((len W) - (2 * n)) + 1 = (((2 * (len ())) + 1) - (2 * n)) + 1 by Def15
.= 2 * rn ;
2 * n <= len () by ;
then A15: 2 * n in dom () by ;
(Rev ()) . n = () . rn by
.= W . (2 * rn) by ;
hence ((W .reverse()) .edgeSeq()) . n = (Rev ()) . n by A15, A6, A14, Lm8; :: thesis: verum
end;
len () = len (Rev ()) by ;
hence (W .reverse()) .edgeSeq() = Rev () by ; :: thesis: verum