deffunc H1( 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 = H1(k) ) ) from 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:
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 ;
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 ;
then 1 * 2 <= 2x by XREAL_1:64;
then reconsider 2xaa1 = 2x - 1 as odd Element of NAT by ;
x <= lenW1 div 2 by ;
then 2x <= (lenW1 div 2) * 2 by XREAL_1:64;
then 2xaa1 <= lenW1 - 1 by ;
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 ;
set 2naa1 = 2n - 1;
1 * 2 <= n * 2 by ;
then reconsider 2naa1 = 2n - 1 as odd Element of NAT by ;
2n <= lenW1 by ;
then A10: 2n - 1 <= ((len W) + 1) - 1 by XREAL_1:9;
2naa1 <> len W by A3, A1, A8;
then 2naa1 < len W by ;
then A11: W . (2naa1 + 1) Joins W . 2naa1,W . (2naa1 + 2),G by Def3;
n + 1 <= lenW1 div 2 by ;
then n + 1 in dom IT by ;
then A12: IT . (n + 1) = W . ((2 * (n + 1)) - 1) by A1
.= W . (2n + 1) ;
n in dom IT by ;
then W . (2naa1 + 1) Joins IT . n,W . (2naa1 + 2),G by ;
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 ; :: 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 ;
hence IT . n = W . ((2 * n) - 1) by A1; :: thesis: verum