set f = W .vertexSeq() ;

now :: thesis: for x1, x2 being object st x1 in dom (W .vertexSeq()) & x2 in dom (W .vertexSeq()) & (W .vertexSeq()) . x1 = (W .vertexSeq()) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (W .vertexSeq()) & x2 in dom (W .vertexSeq()) & (W .vertexSeq()) . x1 = (W .vertexSeq()) . x2 implies x1 = x2 )
assume A8: ( x1 in dom (W .vertexSeq()) & x2 in dom (W .vertexSeq()) & (W .vertexSeq()) . x1 = (W .vertexSeq()) . x2 ) ; :: thesis: x1 = x2
then reconsider n = x1, m = x2 as Nat ;
A9: ( 1 <= n & n <= len (W .vertexSeq()) & 1 <= m & m <= len (W .vertexSeq()) ) by A8, FINSEQ_3:25;
A10: W . ((2 * n) - 1) = (W .vertexSeq()) . x1 by A9, GLIB_001:def 14
.= W . ((2 * m) - 1) by A8, A9, GLIB_001:def 14 ;
( 2 * 1 <= 2 * n & 2 * 1 <= 2 * m ) by A9, XREAL_1:64;
then ( 2 - 1 <= (2 * n) - 1 & 2 - 1 <= (2 * m) - 1 ) by XREAL_1:9;
then ( (2 * n) -' 1 = (2 * n) - 1 & (2 * m) -' 1 = (2 * m) - 1 ) by NAT_D:39;
then A11: ( (2 * n) - 1 is odd Element of NAT & (2 * m) - 1 is odd Element of NAT ) ;
( 2 * n <= 2 * (len (W .vertexSeq())) & 2 * m <= 2 * (len (W .vertexSeq())) ) by A9, XREAL_1:64;
then ( 2 * n <= (len W) + 1 & 2 * m <= (len W) + 1 ) by GLIB_001:def 14;
then ( (2 * n) - 1 <= ((len W) + 1) - 1 & (2 * m) - 1 <= ((len W) + 1) - 1 ) by XREAL_1:9;
then (2 * n) - 1 = (2 * m) - 1 by A10, A11, GLIB_001:def 29;
hence x1 = x2 ; :: thesis: verum

end;

hence W .vertexSeq() is one-to-one by FUNCT_1:def 4; :: thesis: verum