let IT1, IT2 be EdgeSeq of G; :: thesis: ( len W =(2 *(len IT1))+ 1 & ( for n being Nat st 1 <= n & n <=len IT1 holds IT1 . n = W .(2 * n) ) & len W =(2 *(len IT2))+ 1 & ( for n being Nat st 1 <= n & n <=len IT2 holds IT2 . n = W .(2 * n) ) implies IT1 = IT2 ) assume that A20:
len W =(2 *(len IT1))+ 1
and A21:
for n being Nat st 1 <= n & n <=len IT1 holds IT1 . n = W .(2 * n)and A22:
len W =(2 *(len IT2))+ 1
and A23:
for n being Nat st 1 <= n & n <=len IT2 holds IT2 . n = W .(2 * n)
; :: thesis: IT1 = IT2