let G be real-weighted WGraph; :: thesis: for W being Walk of G holds W .cost() = (W .reverse()) .cost()
let W be Walk of G; :: thesis: W .cost() = (W .reverse()) .cost()
thus W .cost() = Sum (Rev (W .weightSeq())) by POLYNOM3:3
.= (W .reverse()) .cost() by Th15 ; :: thesis: verum