let G be _Graph; :: thesis: for W1, W2 being Walk of G holds

( len W1 = len W2 iff W1 .length() = W2 .length() )

let W1, W2 be Walk of G; :: thesis: ( len W1 = len W2 iff W1 .length() = W2 .length() )

hence len W1 = (2 * (W2 .length())) + 1 by Def15

.= len W2 by Def15 ;

:: thesis: verum

( len W1 = len W2 iff W1 .length() = W2 .length() )

let W1, W2 be Walk of G; :: thesis: ( len W1 = len W2 iff W1 .length() = W2 .length() )

hereby :: thesis: ( W1 .length() = W2 .length() implies len W1 = len W2 )

assume
W1 .length() = W2 .length()
; :: thesis: len W1 = len W2assume
len W1 = len W2
; :: thesis: W1 .length() = W2 .length()

then (2 * (W1 .length())) + 1 = len W2 by Def15

.= (2 * (W2 .length())) + 1 by Def15 ;

hence W1 .length() = W2 .length() ; :: thesis: verum

end;then (2 * (W1 .length())) + 1 = len W2 by Def15

.= (2 * (W2 .length())) + 1 by Def15 ;

hence W1 .length() = W2 .length() ; :: thesis: verum

hence len W1 = (2 * (W2 .length())) + 1 by Def15

.= len W2 by Def15 ;

:: thesis: verum