let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1

for W2 being Walk of G2 holds

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

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 holds

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

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

thus len W1 = (2 * (W1 .length())) + 1 by GLIB_001:112

.= len W2 by A2, GLIB_001:112 ; :: thesis: verum

for W2 being Walk of G2 holds

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

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 holds

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

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

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

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

(2 * (W1 .length())) + 1 = len W1 by GLIB_001:112

.= (2 * (W2 .length())) + 1 by A1, GLIB_001:112 ;

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

end;(2 * (W1 .length())) + 1 = len W1 by GLIB_001:112

.= (2 * (W2 .length())) + 1 by A1, GLIB_001:112 ;

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

thus len W1 = (2 * (W1 .length())) + 1 by GLIB_001:112

.= len W2 by A2, GLIB_001:112 ; :: thesis: verum