let G be _Graph; :: thesis: for W being Walk of G holds W .length() = (W .reverse()) .length()

let W be Walk of G; :: thesis: W .length() = (W .reverse()) .length()

A1: len W = (2 * (W .length())) + 1 by GLIB_001:112;

len W = len (W .reverse()) by GLIB_001:21;

then ((2 * (W .length())) + 1) - 1 = ((2 * ((W .reverse()) .length())) + 1) - 1 by A1, GLIB_001:112;

hence W .length() = (W .reverse()) .length() ; :: thesis: verum

let W be Walk of G; :: thesis: W .length() = (W .reverse()) .length()

A1: len W = (2 * (W .length())) + 1 by GLIB_001:112;

len W = len (W .reverse()) by GLIB_001:21;

then ((2 * (W .length())) + 1) - 1 = ((2 * ((W .reverse()) .length())) + 1) - 1 by A1, GLIB_001:112;

hence W .length() = (W .reverse()) .length() ; :: thesis: verum