let G be _Graph; :: thesis: for W being Walk of G holds (W .reverse()) .edgeSeq() = Rev (W .edgeSeq())

let W be Walk of G; :: thesis: (W .reverse()) .edgeSeq() = Rev (W .edgeSeq())

set W1 = (W .reverse()) .edgeSeq() ;

set W2 = Rev (W .edgeSeq());

A1: len W = len (W .reverse()) by FINSEQ_5:def 3;

len W = (2 * (len (W .edgeSeq()))) + 1 by Def15;

then A2: (2 * (len (W .edgeSeq()))) + 1 = (2 * (len ((W .reverse()) .edgeSeq()))) + 1 by A1, Def15;

hence (W .reverse()) .edgeSeq() = Rev (W .edgeSeq()) by A3, FINSEQ_1:14; :: thesis: verum

let W be Walk of G; :: thesis: (W .reverse()) .edgeSeq() = Rev (W .edgeSeq())

set W1 = (W .reverse()) .edgeSeq() ;

set W2 = Rev (W .edgeSeq());

A1: len W = len (W .reverse()) by FINSEQ_5:def 3;

len W = (2 * (len (W .edgeSeq()))) + 1 by Def15;

then A2: (2 * (len (W .edgeSeq()))) + 1 = (2 * (len ((W .reverse()) .edgeSeq()))) + 1 by A1, Def15;

A3: now :: thesis: for n being Nat st 1 <= n & n <= len ((W .reverse()) .edgeSeq()) holds

((W .reverse()) .edgeSeq()) . n = (Rev (W .edgeSeq())) . n

len ((W .reverse()) .edgeSeq()) = len (Rev (W .edgeSeq()))
by A2, FINSEQ_5:def 3;((W .reverse()) .edgeSeq()) . n = (Rev (W .edgeSeq())) . n

let n be Nat; :: thesis: ( 1 <= n & n <= len ((W .reverse()) .edgeSeq()) implies ((W .reverse()) .edgeSeq()) . n = (Rev (W .edgeSeq())) . n )

assume that

A4: 1 <= n and

A5: n <= len ((W .reverse()) .edgeSeq()) ; :: thesis: ((W .reverse()) .edgeSeq()) . n = (Rev (W .edgeSeq())) . n

A6: ((W .reverse()) .edgeSeq()) . n = (W .reverse()) . (2 * n) by A4, A5, Def15;

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

reconsider rn = ((len (W .edgeSeq())) - n) + 1 as Element of NAT by A2, A5, FINSEQ_5:1;

A7: n in Seg (len (W .edgeSeq())) by A2, A4, A5, FINSEQ_1:1;

then A8: rn in Seg (len (W .edgeSeq())) by FINSEQ_5:2;

then A9: 1 <= rn by FINSEQ_1:1;

A10: n in dom (W .edgeSeq()) by A7, FINSEQ_1:def 3;

then A11: 2 * n in dom W by Lm41;

then A12: 1 <= 2 * n by FINSEQ_3:25;

A13: rn <= len (W .edgeSeq()) by A8, FINSEQ_1:1;

A14: ((len W) - (2 * n)) + 1 = (((2 * (len (W .edgeSeq()))) + 1) - (2 * n)) + 1 by Def15

.= 2 * rn ;

2 * n <= len (W .reverse()) by A1, A11, FINSEQ_3:25;

then A15: 2 * n in dom (W .reverse()) by A12, FINSEQ_3:25;

(Rev (W .edgeSeq())) . n = (W .edgeSeq()) . rn by A10, FINSEQ_5:58

.= W . (2 * rn) by A9, A13, Def15 ;

hence ((W .reverse()) .edgeSeq()) . n = (Rev (W .edgeSeq())) . n by A15, A6, A14, Lm8; :: thesis: verum

end;assume that

A4: 1 <= n and

A5: n <= len ((W .reverse()) .edgeSeq()) ; :: thesis: ((W .reverse()) .edgeSeq()) . n = (Rev (W .edgeSeq())) . n

A6: ((W .reverse()) .edgeSeq()) . n = (W .reverse()) . (2 * n) by A4, A5, Def15;

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

reconsider rn = ((len (W .edgeSeq())) - n) + 1 as Element of NAT by A2, A5, FINSEQ_5:1;

A7: n in Seg (len (W .edgeSeq())) by A2, A4, A5, FINSEQ_1:1;

then A8: rn in Seg (len (W .edgeSeq())) by FINSEQ_5:2;

then A9: 1 <= rn by FINSEQ_1:1;

A10: n in dom (W .edgeSeq()) by A7, FINSEQ_1:def 3;

then A11: 2 * n in dom W by Lm41;

then A12: 1 <= 2 * n by FINSEQ_3:25;

A13: rn <= len (W .edgeSeq()) by A8, FINSEQ_1:1;

A14: ((len W) - (2 * n)) + 1 = (((2 * (len (W .edgeSeq()))) + 1) - (2 * n)) + 1 by Def15

.= 2 * rn ;

2 * n <= len (W .reverse()) by A1, A11, FINSEQ_3:25;

then A15: 2 * n in dom (W .reverse()) by A12, FINSEQ_3:25;

(Rev (W .edgeSeq())) . n = (W .edgeSeq()) . rn by A10, FINSEQ_5:58

.= W . (2 * rn) by A9, A13, Def15 ;

hence ((W .reverse()) .edgeSeq()) . n = (Rev (W .edgeSeq())) . n by A15, A6, A14, Lm8; :: thesis: verum

hence (W .reverse()) .edgeSeq() = Rev (W .edgeSeq()) by A3, FINSEQ_1:14; :: thesis: verum