deffunc H1( Nat) -> set = W . (2 * \$1);
reconsider lenWaa1 = (len W) - 1 as even Element of NAT by ;
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 = H1(n) ) ) from
now :: thesis: for y being object st y in rng IT holds
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:
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 ;
reconsider x = x as Element of NAT by A3;
reconsider 2x = 2 * x as even Element of NAT ;
x <= lenIT by ;
then x * 2 <= lenIT * 2 by XREAL_1:64;
then 2x <= lenWaa1 by ;
then A6: 2x + 1 <= lenWaa1 + 1 by XREAL_1:7;
1 <= x by ;
then 1 * 2 <= 2 * x by XREAL_1:64;
then reconsider 2xaa1 = 2x - 1 as odd Element of NAT by ;
2x <= 2x + 1 by NAT_1:11;
then 2x <= len W by ;
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 ; :: thesis: verum
end;
then rng IT c= the_Edges_of G by TARSKI:def 3;
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 ) )
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 ;
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 ;
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 ;
then n * 2 <= len W by ;
then A15: 2naa1 < (len W) - 0 by XREAL_1:15;
n + 1 <= len vs by ;
then vs . (n + 1) = W . ((2 * (n + 1)) - 1) by ;
then A16: vs . (n + 1) = W . (2naa1 + 2) ;
n in dom IT by ;
then A17: IT . n = W . (2naa1 + 1) by A1;
n <= len vs by ;
then vs . n = W . ((2 * n) - 1) by ;
hence IT . n Joins vs . n,vs . (n + 1),G by ; :: thesis: verum
end;
then reconsider IT = IT as EdgeSeq of G by Def2;
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 ;
hence IT . n = W . (2 * n) by A1; :: thesis: verum