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

reconsider lenWaa1 = (len W) - 1 as even Element of NAT by ABIAN:12, INT_1:5;

set lenIT = lenWaa1 div 2;

reconsider lenIT = lenWaa1 div 2 as Element of NAT ;

consider IT being FinSequence such that

A1: ( len IT = lenIT & ( for n being Nat st n in dom IT holds

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

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

2 divides lenWaa1 by PEPIN:22;

then A8: lenWaa1 = 2 * lenIT by NAT_D:3;

then A9: len W = (2 * lenIT) + 1 ;

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

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

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

IT . n = W . (2 * n)

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

assume that

A18: 1 <= n and

A19: n <= len IT ; :: thesis: IT . n = W . (2 * n)

n in dom IT by A18, A19, FINSEQ_3:25;

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

reconsider lenWaa1 = (len W) - 1 as even Element of NAT by ABIAN:12, INT_1:5;

set lenIT = lenWaa1 div 2;

reconsider lenIT = lenWaa1 div 2 as Element of NAT ;

consider IT being FinSequence such that

A1: ( len IT = lenIT & ( for n being Nat st n in dom IT holds

IT . n = H

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

y in the_Edges_of G

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

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

A2: 2 divides lenWaa1 by PEPIN:22;

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

then consider x being object such that

A3: x in dom IT and

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

A5: x in Seg lenIT by A1, A3, FINSEQ_1:def 3;

reconsider x = x as Element of NAT by A3;

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

x <= lenIT by A5, FINSEQ_1:1;

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

then 2x <= lenWaa1 by A2, NAT_D:3;

then A6: 2x + 1 <= lenWaa1 + 1 by XREAL_1:7;

1 <= x by A5, FINSEQ_1:1;

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

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

2x <= 2x + 1 by NAT_1:11;

then 2x <= len W by A6, XXREAL_0:2;

then 2xaa1 < len W by XREAL_1:147;

then A7: W . (2xaa1 + 1) Joins W . 2xaa1,W . (2xaa1 + 2),G by Def3;

y = W . (2 * x) by A1, A3, A4;

hence y in the_Edges_of G by A7, GLIB_000:def 13; :: thesis: verum

end;A2: 2 divides lenWaa1 by PEPIN:22;

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

then consider x being object such that

A3: x in dom IT and

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

A5: x in Seg lenIT by A1, A3, FINSEQ_1:def 3;

reconsider x = x as Element of NAT by A3;

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

x <= lenIT by A5, FINSEQ_1:1;

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

then 2x <= lenWaa1 by A2, NAT_D:3;

then A6: 2x + 1 <= lenWaa1 + 1 by XREAL_1:7;

1 <= x by A5, FINSEQ_1:1;

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

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

2x <= 2x + 1 by NAT_1:11;

then 2x <= len W by A6, XXREAL_0:2;

then 2xaa1 < len W by XREAL_1:147;

then A7: W . (2xaa1 + 1) Joins W . 2xaa1,W . (2xaa1 + 2),G by Def3;

y = W . (2 * x) by A1, A3, A4;

hence y in the_Edges_of G by A7, GLIB_000:def 13; :: thesis: verum

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

2 divides lenWaa1 by PEPIN:22;

then A8: lenWaa1 = 2 * lenIT by NAT_D:3;

then A9: len W = (2 * lenIT) + 1 ;

now :: thesis: ex vs being VertexSeq of G st

( len vs = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len IT holds

IT . n Joins vs . n,vs . (n + 1),G ) )

then reconsider IT = IT as EdgeSeq of G by Def2;( len vs = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len IT holds

IT . n Joins vs . n,vs . (n + 1),G ) )

set vs = W .vertexSeq() ;

take vs = W .vertexSeq() ; :: thesis: ( len vs = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len IT holds

IT . n Joins vs . n,vs . (n + 1),G ) )

A10: ((2 * (len IT)) + 1) + 1 = 2 * (len vs) by A8, A1, Def14;

then A11: 2 * ((len IT) + 1) = 2 * (len vs) ;

thus len vs = (len IT) + 1 by A10; :: thesis: for n being Element of NAT st 1 <= n & n <= len IT holds

IT . n Joins vs . n,vs . (n + 1),G

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len IT implies IT . n Joins vs . n,vs . (n + 1),G )

set v1 = vs . n;

set v2 = vs . (n + 1);

assume that

A12: 1 <= n and

A13: n <= len IT ; :: thesis: IT . n Joins vs . n,vs . (n + 1),G

set 2n = 2 * n;

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

set 2naa1 = 2n - 1;

1 <= n + n by A12, NAT_1:12;

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

A14: 1 <= n + 1 by NAT_1:12;

n * 2 <= (len IT) * 2 by A13, XREAL_1:64;

then n * 2 <= len W by A9, A1, NAT_1:12;

then A15: 2naa1 < (len W) - 0 by XREAL_1:15;

n + 1 <= len vs by A11, A13, XREAL_1:7;

then vs . (n + 1) = W . ((2 * (n + 1)) - 1) by A14, Def14;

then A16: vs . (n + 1) = W . (2naa1 + 2) ;

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

then A17: IT . n = W . (2naa1 + 1) by A1;

n <= len vs by A11, A13, NAT_1:12;

then vs . n = W . ((2 * n) - 1) by A12, Def14;

hence IT . n Joins vs . n,vs . (n + 1),G by A17, A16, A15, Def3; :: thesis: verum

end;take vs = W .vertexSeq() ; :: thesis: ( len vs = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len IT holds

IT . n Joins vs . n,vs . (n + 1),G ) )

A10: ((2 * (len IT)) + 1) + 1 = 2 * (len vs) by A8, A1, Def14;

then A11: 2 * ((len IT) + 1) = 2 * (len vs) ;

thus len vs = (len IT) + 1 by A10; :: thesis: for n being Element of NAT st 1 <= n & n <= len IT holds

IT . n Joins vs . n,vs . (n + 1),G

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len IT implies IT . n Joins vs . n,vs . (n + 1),G )

set v1 = vs . n;

set v2 = vs . (n + 1);

assume that

A12: 1 <= n and

A13: n <= len IT ; :: thesis: IT . n Joins vs . n,vs . (n + 1),G

set 2n = 2 * n;

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

set 2naa1 = 2n - 1;

1 <= n + n by A12, NAT_1:12;

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

A14: 1 <= n + 1 by NAT_1:12;

n * 2 <= (len IT) * 2 by A13, XREAL_1:64;

then n * 2 <= len W by A9, A1, NAT_1:12;

then A15: 2naa1 < (len W) - 0 by XREAL_1:15;

n + 1 <= len vs by A11, A13, XREAL_1:7;

then vs . (n + 1) = W . ((2 * (n + 1)) - 1) by A14, Def14;

then A16: vs . (n + 1) = W . (2naa1 + 2) ;

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

then A17: IT . n = W . (2naa1 + 1) by A1;

n <= len vs by A11, A13, NAT_1:12;

then vs . n = W . ((2 * n) - 1) by A12, Def14;

hence IT . n Joins vs . n,vs . (n + 1),G by A17, A16, A15, Def3; :: thesis: verum

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

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

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

IT . n = W . (2 * n)

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

assume that

A18: 1 <= n and

A19: n <= len IT ; :: thesis: IT . n = W . (2 * n)

n in dom IT by A18, A19, FINSEQ_3:25;

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