deffunc H_{1}( Nat) -> set = W . ((2 * $1) - 1);

reconsider lenW1 = (len W) + 1 as even Element of NAT ;

set lenIT = lenW1 div 2;

consider IT being FinSequence such that

A1: ( len IT = lenW1 div 2 & ( for k being Nat st k in dom IT holds

IT . k = H_{1}(k) ) )
from FINSEQ_1:sch 2();

A2: 2 divides lenW1 by PEPIN:22;

then A3: 2 * (lenW1 div 2) = lenW1 by NAT_D:3;

then reconsider IT = IT as FinSequence of the_Vertices_of G by FINSEQ_1:def 4;

take IT ; :: thesis: ( (len W) + 1 = 2 * (len IT) & ( for n being Nat st 1 <= n & n <= len IT holds

IT . n = W . ((2 * n) - 1) ) )

thus (len W) + 1 = 2 * (len IT) by A2, A1, NAT_D:3; :: thesis: for n being Nat st 1 <= n & n <= len IT holds

IT . n = W . ((2 * n) - 1)

let n be Nat; :: thesis: ( 1 <= n & n <= len IT implies IT . n = W . ((2 * n) - 1) )

assume that

A13: 1 <= n and

A14: n <= len IT ; :: thesis: IT . n = W . ((2 * n) - 1)

n in dom IT by A13, A14, FINSEQ_3:25;

hence IT . n = W . ((2 * n) - 1) by A1; :: thesis: verum

reconsider lenW1 = (len W) + 1 as even Element of NAT ;

set lenIT = lenW1 div 2;

consider IT being FinSequence such that

A1: ( len IT = lenW1 div 2 & ( for k being Nat st k in dom IT holds

IT . k = H

A2: 2 divides lenW1 by PEPIN:22;

then A3: 2 * (lenW1 div 2) = lenW1 by NAT_D:3;

now :: thesis: for y being object st y in rng IT holds

y in the_Vertices_of G

then
rng IT c= the_Vertices_of G
by TARSKI:def 3;y in the_Vertices_of G

let y be object ; :: thesis: ( y in rng IT implies y in the_Vertices_of G )

assume y in rng IT ; :: thesis: y in the_Vertices_of G

then consider x being object such that

A4: x in dom IT and

A5: y = IT . x by FUNCT_1:def 3;

A6: x in Seg (lenW1 div 2) by A1, A4, FINSEQ_1:def 3;

reconsider x = x as Element of NAT by A4;

set 2x = x * 2;

reconsider 2x = x * 2 as even Element of NAT ;

set 2xaa1 = 2x - 1;

1 <= x by A6, FINSEQ_1:1;

then 1 * 2 <= 2x by XREAL_1:64;

then reconsider 2xaa1 = 2x - 1 as odd Element of NAT by INT_1:5, XXREAL_0:2;

x <= lenW1 div 2 by A6, FINSEQ_1:1;

then 2x <= (lenW1 div 2) * 2 by XREAL_1:64;

then 2xaa1 <= lenW1 - 1 by A3, XREAL_1:9;

then W . 2xaa1 = W .vertexAt 2xaa1 by Def8;

then W . 2xaa1 in the_Vertices_of G ;

hence y in the_Vertices_of G by A1, A4, A5; :: thesis: verum

end;assume y in rng IT ; :: thesis: y in the_Vertices_of G

then consider x being object such that

A4: x in dom IT and

A5: y = IT . x by FUNCT_1:def 3;

A6: x in Seg (lenW1 div 2) by A1, A4, FINSEQ_1:def 3;

reconsider x = x as Element of NAT by A4;

set 2x = x * 2;

reconsider 2x = x * 2 as even Element of NAT ;

set 2xaa1 = 2x - 1;

1 <= x by A6, FINSEQ_1:1;

then 1 * 2 <= 2x by XREAL_1:64;

then reconsider 2xaa1 = 2x - 1 as odd Element of NAT by INT_1:5, XXREAL_0:2;

x <= lenW1 div 2 by A6, FINSEQ_1:1;

then 2x <= (lenW1 div 2) * 2 by XREAL_1:64;

then 2xaa1 <= lenW1 - 1 by A3, XREAL_1:9;

then W . 2xaa1 = W .vertexAt 2xaa1 by Def8;

then W . 2xaa1 in the_Vertices_of G ;

hence y in the_Vertices_of G by A1, A4, A5; :: thesis: verum

then reconsider IT = IT as FinSequence of the_Vertices_of G by FINSEQ_1:def 4;

now :: thesis: for n being Element of NAT st 1 <= n & n < len IT holds

ex e being set st e Joins IT . n,IT . (n + 1),G

then reconsider IT = IT as VertexSeq of G by Def1;ex e being set st e Joins IT . n,IT . (n + 1),G

let n be Element of NAT ; :: thesis: ( 1 <= n & n < len IT implies ex e being set st e Joins IT . n,IT . (n + 1),G )

set v2 = IT . (n + 1);

assume that

A7: 1 <= n and

A8: n < len IT ; :: thesis: ex e being set st e Joins IT . n,IT . (n + 1),G

set 2n = 2 * n;

reconsider 2n = 2 * n as even Element of NAT ;

A9: 1 <= n + 1 by A7, NAT_1:13;

set 2naa1 = 2n - 1;

1 * 2 <= n * 2 by A7, XREAL_1:64;

then reconsider 2naa1 = 2n - 1 as odd Element of NAT by INT_1:5, XXREAL_0:2;

2n <= lenW1 by A3, A1, A8, XREAL_1:68;

then A10: 2n - 1 <= ((len W) + 1) - 1 by XREAL_1:9;

2naa1 <> len W by A3, A1, A8;

then 2naa1 < len W by A10, XXREAL_0:1;

then A11: W . (2naa1 + 1) Joins W . 2naa1,W . (2naa1 + 2),G by Def3;

n + 1 <= lenW1 div 2 by A1, A8, NAT_1:13;

then n + 1 in dom IT by A1, A9, FINSEQ_3:25;

then A12: IT . (n + 1) = W . ((2 * (n + 1)) - 1) by A1

.= W . (2n + 1) ;

n in dom IT by A7, A8, FINSEQ_3:25;

then W . (2naa1 + 1) Joins IT . n,W . (2naa1 + 2),G by A1, A11;

hence ex e being set st e Joins IT . n,IT . (n + 1),G by A12; :: thesis: verum

end;set v2 = IT . (n + 1);

assume that

A7: 1 <= n and

A8: n < len IT ; :: thesis: ex e being set st e Joins IT . n,IT . (n + 1),G

set 2n = 2 * n;

reconsider 2n = 2 * n as even Element of NAT ;

A9: 1 <= n + 1 by A7, NAT_1:13;

set 2naa1 = 2n - 1;

1 * 2 <= n * 2 by A7, XREAL_1:64;

then reconsider 2naa1 = 2n - 1 as odd Element of NAT by INT_1:5, XXREAL_0:2;

2n <= lenW1 by A3, A1, A8, XREAL_1:68;

then A10: 2n - 1 <= ((len W) + 1) - 1 by XREAL_1:9;

2naa1 <> len W by A3, A1, A8;

then 2naa1 < len W by A10, XXREAL_0:1;

then A11: W . (2naa1 + 1) Joins W . 2naa1,W . (2naa1 + 2),G by Def3;

n + 1 <= lenW1 div 2 by A1, A8, NAT_1:13;

then n + 1 in dom IT by A1, A9, FINSEQ_3:25;

then A12: IT . (n + 1) = W . ((2 * (n + 1)) - 1) by A1

.= W . (2n + 1) ;

n in dom IT by A7, A8, FINSEQ_3:25;

then W . (2naa1 + 1) Joins IT . n,W . (2naa1 + 2),G by A1, A11;

hence ex e being set st e Joins IT . n,IT . (n + 1),G by A12; :: thesis: verum

take IT ; :: thesis: ( (len W) + 1 = 2 * (len IT) & ( for n being Nat st 1 <= n & n <= len IT holds

IT . n = W . ((2 * n) - 1) ) )

thus (len W) + 1 = 2 * (len IT) by A2, A1, NAT_D:3; :: thesis: for n being Nat st 1 <= n & n <= len IT holds

IT . n = W . ((2 * n) - 1)

let n be Nat; :: thesis: ( 1 <= n & n <= len IT implies IT . n = W . ((2 * n) - 1) )

assume that

A13: 1 <= n and

A14: n <= len IT ; :: thesis: IT . n = W . ((2 * n) - 1)

n in dom IT by A13, A14, FINSEQ_3:25;

hence IT . n = W . ((2 * n) - 1) by A1; :: thesis: verum