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()

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() ) )

hence
W .edges() = (W .reverse()) .edges()
by TARSKI:2; :: thesis: verum( ( 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() ) )

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;hereby :: thesis: ( e in (W .reverse()) .edges() implies e in W .edges() )

assume
e in (W .reverse()) .edges()
; :: thesis: 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;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

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