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 A20, FINSEQ_3:25;
A22: 1 <= n by A20, FINSEQ_3:25;
then IT1 . n = W . ((2 * n) - 1) by A16, A21;
hence IT1 . n = IT2 . n by A15, A17, A18, A22, A21; :: thesis: verum

end;

dom IT1 = Seg (len IT2) by A15, A17, FINSEQ_1:def 3
.= dom IT2 by FINSEQ_1:def 3 ;
hence IT1 = IT2 by A19, FINSEQ_1:13; :: thesis: verum