let IT1, IT2 be VertexSeq of G; :: thesis: ( (len W) + 1 = 2 * (len IT1) & ( for n being Nat st 1 <= n & n <= len IT1 holds
IT1 . n = W . ((2 * n) - 1) ) & (len W) + 1 = 2 * (len IT2) & ( for n being Nat st 1 <= n & n <= len IT2 holds
IT2 . n = W . ((2 * n) - 1) ) implies IT1 = IT2 )

assume that
A15: (len W) + 1 = 2 * (len IT1) and
A16: for n being Nat st 1 <= n & n <= len IT1 holds
IT1 . n = W . ((2 * n) - 1) and
A17: (len W) + 1 = 2 * (len IT2) and
A18: for n being Nat st 1 <= n & n <= len IT2 holds
IT2 . n = W . ((2 * n) - 1) ; :: thesis: IT1 = IT2
A19: now :: thesis: for n being Nat st n in dom IT1 holds
IT1 . n = IT2 . n
let n be Nat; :: thesis: ( n in dom IT1 implies IT1 . n = IT2 . n )
assume A20: n in dom IT1 ; :: thesis: IT1 . n = IT2 . n
A21: n <= len IT1 by ;
A22: 1 <= n by ;
then IT1 . n = W . ((2 * n) - 1) by ;
hence IT1 . n = IT2 . n by A15, A17, A18, A22, A21; :: thesis: verum
end;
dom IT1 = Seg (len IT2) by
.= dom IT2 by FINSEQ_1:def 3 ;
hence IT1 = IT2 by ; :: thesis: verum