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

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;

then rng IT c= the_Vertices_of G by TARSKI:def 3;
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

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;

then reconsider IT = IT as VertexSeq of G by Def1;
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