let G be _Graph; :: thesis: for W being Walk of G holds W .edges() = (W .reverse()) .edges()
let W be Walk of G; :: thesis: W .edges() = (W .reverse()) .edges()
now :: thesis: for e being object holds
( ( e in W .edges() implies e in (W .reverse()) .edges() ) & ( e in (W .reverse()) .edges() implies e in W .edges() ) )
let e be object ; :: thesis: ( ( e in W .edges() implies e in (W .reverse()) .edges() ) & ( e in (W .reverse()) .edges() implies e in W .edges() ) )
hereby :: thesis: ( e in (W .reverse()) .edges() implies e in W .edges() )
assume e in W .edges() ; :: thesis: e in (W .reverse()) .edges()
then consider n being even Element of NAT such that
A1: 1 <= n and
A2: n <= len W and
A3: W . n = e by Lm46;
A4: n in dom W by A1, A2, FINSEQ_3:25;
then A5: ((len W) - n) + 1 in dom (W .reverse()) by Th23;
then reconsider rn = ((len W) - n) + 1 as even Element of NAT ;
A6: 1 <= rn by A5, FINSEQ_3:25;
A7: rn <= len (W .reverse()) by A5, FINSEQ_3:25;
e = (W .reverse()) . (((len W) - n) + 1) by A3, A4, Th23;
hence e in (W .reverse()) .edges() by A6, A7, Lm46; :: thesis: verum
end;
assume e in (W .reverse()) .edges() ; :: thesis: e in W .edges()
then consider n being even Element of NAT such that
A8: 1 <= n and
A9: n <= len (W .reverse()) and
A10: (W .reverse()) . n = e by Lm46;
A11: n in dom (W .reverse()) by A8, A9, FINSEQ_3:25;
then A12: ((len (W .reverse())) - n) + 1 in dom ((W .reverse()) .reverse()) by Th23;
then reconsider rn = ((len (W .reverse())) - n) + 1 as even Element of NAT ;
e = ((W .reverse()) .reverse()) . (((len (W .reverse())) - n) + 1) by A10, A11, Th23;
then A13: e = W . rn ;
rn in dom W by A12;
then A14: rn <= len W by FINSEQ_3:25;
1 <= rn by A12, FINSEQ_3:25;
hence e in W .edges() by A13, A14, Lm46; :: thesis: verum
end;
hence W .edges() = (W .reverse()) .edges() by TARSKI:2; :: thesis: verum