hereby :: thesis: ( not v in W .vertices() implies ex b_{1} being odd Element of NAT st b_{1} = len W )

set IT = len W;defpred S_{1}[ Nat] means ( $1 is odd & $1 <= len W & W . $1 = v );

set vs = W .vertexSeq() ;

assume A1: v in W .vertices() ; :: thesis: ex IT being odd Element of NAT st

( IT <= len W & W . IT = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT <= n ) )

_{1}[k]
;

consider IT being Nat such that

A7: ( S_{1}[IT] & ( for n being Nat st S_{1}[n] holds

IT <= n ) ) from NAT_1:sch 5(A6);

reconsider IT = IT as odd Element of NAT by A7, ORDINAL1:def 12;

take IT = IT; :: thesis: ( IT <= len W & W . IT = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT <= n ) )

thus ( IT <= len W & W . IT = v ) by A7; :: thesis: for n being odd Nat st n <= len W & W . n = v holds

IT <= n

let n be odd Nat; :: thesis: ( n <= len W & W . n = v implies IT <= n )

assume that

A8: n <= len W and

A9: W . n = v ; :: thesis: IT <= n

thus IT <= n by A7, A8, A9; :: thesis: verum

end;set vs = W .vertexSeq() ;

assume A1: v in W .vertices() ; :: thesis: ex IT being odd Element of NAT st

( IT <= len W & W . IT = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT <= n ) )

now :: thesis: ex n being odd Element of NAT st

( n <= len W & W . n = v )

then A6:
ex k being Nat st S( n <= len W & W . n = v )

consider i being Nat such that

A2: i in dom (W .vertexSeq()) and

A3: (W .vertexSeq()) . i = v by A1, FINSEQ_2:10;

set n1 = 2 * i;

reconsider n1 = 2 * i as even Nat ;

set n = n1 - 1;

A4: 1 <= i by A2, FINSEQ_3:25;

then 1 <= i + i by NAT_1:12;

then reconsider n = n1 - 1 as odd Element of NAT by INT_1:5;

take n = n; :: thesis: ( n <= len W & W . n = v )

A5: i <= len (W .vertexSeq()) by A2, FINSEQ_3:25;

then i * 2 <= (len (W .vertexSeq())) * 2 by XREAL_1:64;

then i * 2 <= (len W) + 1 by Def14;

then n1 - 1 <= ((len W) + 1) - 1 by XREAL_1:13;

hence n <= len W ; :: thesis: W . n = v

thus W . n = v by A3, A4, A5, Def14; :: thesis: verum

end;A2: i in dom (W .vertexSeq()) and

A3: (W .vertexSeq()) . i = v by A1, FINSEQ_2:10;

set n1 = 2 * i;

reconsider n1 = 2 * i as even Nat ;

set n = n1 - 1;

A4: 1 <= i by A2, FINSEQ_3:25;

then 1 <= i + i by NAT_1:12;

then reconsider n = n1 - 1 as odd Element of NAT by INT_1:5;

take n = n; :: thesis: ( n <= len W & W . n = v )

A5: i <= len (W .vertexSeq()) by A2, FINSEQ_3:25;

then i * 2 <= (len (W .vertexSeq())) * 2 by XREAL_1:64;

then i * 2 <= (len W) + 1 by Def14;

then n1 - 1 <= ((len W) + 1) - 1 by XREAL_1:13;

hence n <= len W ; :: thesis: W . n = v

thus W . n = v by A3, A4, A5, Def14; :: thesis: verum

consider IT being Nat such that

A7: ( S

IT <= n ) ) from NAT_1:sch 5(A6);

reconsider IT = IT as odd Element of NAT by A7, ORDINAL1:def 12;

take IT = IT; :: thesis: ( IT <= len W & W . IT = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT <= n ) )

thus ( IT <= len W & W . IT = v ) by A7; :: thesis: for n being odd Nat st n <= len W & W . n = v holds

IT <= n

let n be odd Nat; :: thesis: ( n <= len W & W . n = v implies IT <= n )

assume that

A8: n <= len W and

A9: W . n = v ; :: thesis: IT <= n

thus IT <= n by A7, A8, A9; :: thesis: verum

assume not v in W .vertices() ; :: thesis: ex b

take len W ; :: thesis: len W = len W

thus len W = len W ; :: thesis: verum