let G be WGraph; for W being Walk of G holds (W .reverse()) .weightSeq() = Rev (W .weightSeq())
let W be Walk of G; (W .reverse()) .weightSeq() = Rev (W .weightSeq())
set W1 = (W .reverse()) .weightSeq() ;
set W2 = Rev (W .weightSeq());
len (W .reverse()) = len W
by GLIB_001:21;
then
(W .reverse()) .length() = W .length()
by GLIB_001:113;
then len ((W .reverse()) .edgeSeq()) =
W .length()
by GLIB_001:def 18
.=
len (W .edgeSeq())
by GLIB_001:def 18
;
then A1:
len ((W .reverse()) .weightSeq()) = len (W .edgeSeq())
by Def18;
A2:
len (W .weightSeq()) = len (W .edgeSeq())
by Def18;
A3:
now for n being Nat st 1 <= n & n <= len ((W .reverse()) .weightSeq()) holds
((W .reverse()) .weightSeq()) . n = (Rev (W .weightSeq())) . nlet n be
Nat;
( 1 <= n & n <= len ((W .reverse()) .weightSeq()) implies ((W .reverse()) .weightSeq()) . n = (Rev (W .weightSeq())) . n )assume that A4:
1
<= n
and A5:
n <= len ((W .reverse()) .weightSeq())
;
((W .reverse()) .weightSeq()) . n = (Rev (W .weightSeq())) . nA6:
n in dom (W .edgeSeq())
by A1, A4, A5, FINSEQ_3:25;
set rn =
((len (W .weightSeq())) - n) + 1;
reconsider rn =
((len (W .weightSeq())) - n) + 1 as
Element of
NAT by A1, A2, A5, FINSEQ_5:1;
n in Seg (len (W .weightSeq()))
by A1, A2, A4, A5, FINSEQ_1:1;
then
rn in Seg (len (W .weightSeq()))
by FINSEQ_5:2;
then A7:
( 1
<= rn &
rn <= len (W .weightSeq()) )
by FINSEQ_1:1;
((W .reverse()) .weightSeq()) . n =
(the_Weight_of G) . (((W .reverse()) .edgeSeq()) . n)
by A4, A5, Def18
.=
(the_Weight_of G) . ((Rev (W .edgeSeq())) . n)
by GLIB_001:84
;
then A8:
((W .reverse()) .weightSeq()) . n = (the_Weight_of G) . ((W .edgeSeq()) . (((len (W .edgeSeq())) - n) + 1))
by A6, FINSEQ_5:58;
n in dom (W .weightSeq())
by A1, A2, A4, A5, FINSEQ_3:25;
then (Rev (W .weightSeq())) . n =
(W .weightSeq()) . rn
by FINSEQ_5:58
.=
(the_Weight_of G) . ((W .edgeSeq()) . rn)
by A7, Def18
;
hence
((W .reverse()) .weightSeq()) . n = (Rev (W .weightSeq())) . n
by A8, Def18;
verum end;
len ((W .reverse()) .weightSeq()) = len (Rev (W .weightSeq()))
by A1, A2, FINSEQ_5:def 3;
hence
(W .reverse()) .weightSeq() = Rev (W .weightSeq())
by A3, FINSEQ_1:14; verum