reconsider lenW1 = (len W) + 1 as even Element of NAT ;
set lenIT = lenW1 div 2;
A1: 2 divides lenW1 by PEPIN:22;
then A2: 2 * (lenW1 div 2) = lenW1 by NAT_D:3;
deffunc H₁( Nat) -> set = W . ((2 * $1) - 1);
consider IT being FinSequence such that
A3: ( len IT = lenW1 div 2 & ( for k being Nat st k in dom IT holds
IT . k = H₁(k) ) ) from FINSEQ_1:sch 2();

now

let y be set ; :: 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 set such that
A4: ( x in dom IT & y = IT . x ) by FUNCT_1:def 5;
A5: x in Seg (lenW1 div 2) by A3, 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 & x <= lenW1 div 2 ) by A5, FINSEQ_1:3;
then A6: ( 1 * 2 <= 2x & 2x <= (lenW1 div 2) * 2 ) by XREAL_1:66;
then reconsider 2xaa1 = 2x - 1 as odd Element of NAT by INT_1:18, XXREAL_0:2;
( 2 - 1 <= 2xaa1 & 2xaa1 <= lenW1 - 1 ) by A2, A6, XREAL_1:11;
then W . 2xaa1 = W .vertexAt 2xaa1 by Def8;
then W . 2xaa1 in the_Vertices_of G ;
hence y in the_Vertices_of G by A3, A4; :: 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

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 A7: ( 1 <= n & n < len IT ) ; :: thesis: ex e being set st e Joins IT . n,IT . (n + 1),G
then A8: n in dom IT by FINSEQ_3:27;
set 2n = 2 * n;
reconsider 2n = 2 * n as even Element of NAT ;
set 2naa1 = 2n - 1;
( 1 <= 2 & 1 * 2 <= n * 2 ) by A7, XREAL_1:66;
then reconsider 2naa1 = 2n - 1 as odd Element of NAT by INT_1:18, XXREAL_0:2;
( 1 <= n + 1 & n + 1 <= lenW1 div 2 ) by A3, A7, NAT_1:13;
then n + 1 in dom IT by A3, FINSEQ_3:27;
then A9: IT . (n + 1) = W . ((2 * (n + 1)) - 1) by A3
.= W . (2n + 1) ;
( 2n <= lenW1 & 2n <> lenW1 ) by A2, A3, A7, XREAL_1:70;
then A10: 2n - 1 <= ((len W) + 1) - 1 by XREAL_1:11;
2naa1 <> len W by A2, A3, A7;
then 2naa1 < len W by A10, XXREAL_0:1;
then W . (2naa1 + 1) Joins W . 2naa1,W . (2naa1 + 2),G by Def3;
then W . (2naa1 + 1) Joins IT . n,W . (2naa1 + 2),G by A3, A8;
hence ex e being set st e Joins IT . n,IT . (n + 1),G by A9; :: 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 A1, A3, 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 ( 1 <= n & n <= len IT ) ; :: thesis: IT . n = W . ((2 * n) - 1)
then n in dom IT by FINSEQ_3:27;
hence IT . n = W . ((2 * n) - 1) by A3; :: thesis: verum