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;
then A3:
len ((W .reverse() ) .edgeSeq() ) = len (Rev (W .edgeSeq() ))
by FINSEQ_5:def 3;
now let n be
Nat;
:: thesis: ( 1 <= n & n <= len ((W .reverse() ) .edgeSeq() ) implies ((W .reverse() ) .edgeSeq() ) . n = (Rev (W .edgeSeq() )) . n )assume A4:
( 1
<= n &
n <= len ((W .reverse() ) .edgeSeq() ) )
;
:: thesis: ((W .reverse() ) .edgeSeq() ) . n = (Rev (W .edgeSeq() )) . nset rn =
((len (W .edgeSeq() )) - n) + 1;
reconsider rn =
((len (W .edgeSeq() )) - n) + 1 as
Element of
NAT by A2, A4, FINSEQ_5:1;
A5:
n in Seg (len (W .edgeSeq() ))
by A2, A4, FINSEQ_1:3;
then
rn in Seg (len (W .edgeSeq() ))
by FINSEQ_5:2;
then A6:
( 1
<= rn &
rn <= len (W .edgeSeq() ) )
by FINSEQ_1:3;
A7:
n in dom (W .edgeSeq() )
by A5, FINSEQ_1:def 3;
then A8:
(Rev (W .edgeSeq() )) . n =
(W .edgeSeq() ) . rn
by FINSEQ_5:61
.=
W . (2 * rn)
by A6, Def15
;
2
* n in dom W
by A7, Lm41;
then
( 1
<= 2
* n & 2
* n <= len (W .reverse() ) )
by A1, FINSEQ_3:27;
then A9:
2
* n in dom (W .reverse() )
by FINSEQ_3:27;
A10:
((W .reverse() ) .edgeSeq() ) . n = (W .reverse() ) . (2 * n)
by A4, Def15;
((len W) - (2 * n)) + 1 =
(((2 * (len (W .edgeSeq() ))) + 1) - (2 * n)) + 1
by Def15
.=
2
* rn
;
hence
((W .reverse() ) .edgeSeq() ) . n = (Rev (W .edgeSeq() )) . n
by A8, A9, A10, Lm8;
:: thesis: verum end;
hence
(W .reverse() ) .edgeSeq() = Rev (W .edgeSeq() )
by A3, FINSEQ_1:18; :: thesis: verum