deffunc H₁( 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₁(n) ) ) from FINSEQ_1:sch 2();

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: 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;

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 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;

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 A18, A19, FINSEQ_3:25;
hence IT . n = W . (2 * n) by A1; :: thesis: verum