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

.= dom IT2 by FINSEQ_1:def 3 ;

hence IT1 = IT2 by A19, FINSEQ_1:13; :: thesis: verum

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

dom IT1 =
Seg (len IT2)
by A15, A17, FINSEQ_1:def 3
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;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

.= dom IT2 by FINSEQ_1:def 3 ;

hence IT1 = IT2 by A19, FINSEQ_1:13; :: thesis: verum