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:22;
then
(W .reverse() ) .length() = W .length()
by GLIB_001:114;
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;
then A3:
len ((W .reverse() ) .weightSeq() ) = len (Rev (W .weightSeq() ))
by A1, FINSEQ_5:def 3;
now let n be
Nat;
:: thesis: ( 1 <= n & n <= len ((W .reverse() ) .weightSeq() ) implies ((W .reverse() ) .weightSeq() ) . n = (Rev (W .weightSeq() )) . n )assume A4:
( 1
<= n &
n <= len ((W .reverse() ) .weightSeq() ) )
;
:: thesis: ((W .reverse() ) .weightSeq() ) . n = (Rev (W .weightSeq() )) . nthen A5:
((W .reverse() ) .weightSeq() ) . n =
(the_Weight_of G) . (((W .reverse() ) .edgeSeq() ) . n)
by Def18
.=
(the_Weight_of G) . ((Rev (W .edgeSeq() )) . n)
by GLIB_001:85
;
n in dom (W .edgeSeq() )
by A1, A4, FINSEQ_3:27;
then A6:
((W .reverse() ) .weightSeq() ) . n = (the_Weight_of G) . ((W .edgeSeq() ) . (((len (W .edgeSeq() )) - n) + 1))
by A5, FINSEQ_5:61;
set rn =
((len (W .weightSeq() )) - n) + 1;
reconsider rn =
((len (W .weightSeq() )) - n) + 1 as
Element of
NAT by A1, A2, A4, FINSEQ_5:1;
n in Seg (len (W .weightSeq() ))
by A1, A2, A4, FINSEQ_1:3;
then
rn in Seg (len (W .weightSeq() ))
by FINSEQ_5:2;
then A7:
( 1
<= rn &
rn <= len (W .weightSeq() ) )
by FINSEQ_1:3;
n in dom (W .weightSeq() )
by A1, A2, A4, FINSEQ_3:27;
then (Rev (W .weightSeq() )) . n =
(W .weightSeq() ) . rn
by FINSEQ_5:61
.=
(the_Weight_of G) . ((W .edgeSeq() ) . rn)
by A7, Def18
;
hence
((W .reverse() ) .weightSeq() ) . n = (Rev (W .weightSeq() )) . n
by A6, Def18;
:: thesis: verum end;
hence
(W .reverse() ) .weightSeq() = Rev (W .weightSeq() )
by A3, FINSEQ_1:18; :: thesis: verum