let G1, G2 be _Graph; for W1 being Walk of G1
for W2 being Walk of G2
for m, n being Element of NAT st W1 = W2 holds
W1 .cut (m,n) = W2 .cut (m,n)
let W1 be Walk of G1; for W2 being Walk of G2
for m, n being Element of NAT st W1 = W2 holds
W1 .cut (m,n) = W2 .cut (m,n)
let W2 be Walk of G2; for m, n being Element of NAT st W1 = W2 holds
W1 .cut (m,n) = W2 .cut (m,n)
let m, n be Element of NAT ; ( W1 = W2 implies W1 .cut (m,n) = W2 .cut (m,n) )
assume A1:
W1 = W2
; W1 .cut (m,n) = W2 .cut (m,n)
hence
W1 .cut (m,n) = W2 .cut (m,n)
; verum