let G be WGraph; :: thesis: for W being Walk of G holds (W .reverse()) .weightSeq() = Rev (W .weightSeq())
let W be Walk of G; :: thesis: (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 :: thesis: for n being Nat st 1 <= n & n <= len ((W .reverse()) .weightSeq()) holds
((W .reverse()) .weightSeq()) . n = (Rev (W .weightSeq())) . n

let n be Nat; :: thesis: ( 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()) ; :: thesis: ((W .reverse()) .weightSeq()) . n = (Rev (W .weightSeq())) . n
A6: 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; :: thesis: 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; :: thesis: verum