let G be _Graph; for W being Walk of G holds (W .reverse()) .edgeSeq() = Rev (W .edgeSeq())
let W be Walk of G; (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 for n being Nat st 1 <= n & n <= len ((W .reverse()) .edgeSeq()) holds
((W .reverse()) .edgeSeq()) . n = (Rev (W .edgeSeq())) . nlet n be
Nat;
( 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())
;
((W .reverse()) .edgeSeq()) . n = (Rev (W .edgeSeq())) . nA6:
((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;
verum end;
len ((W .reverse()) .edgeSeq()) = len (Rev (W .edgeSeq()))
by A2, FINSEQ_5:def 3;
hence
(W .reverse()) .edgeSeq() = Rev (W .edgeSeq())
by A3, FINSEQ_1:14; verum