deffunc H1( 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 = H1(n) ) )
from FINSEQ_1:sch 2();
now for y being object st y in rng IT holds
y in the_Edges_of Glet y be
object ;
( y in rng IT implies y in the_Edges_of G )A2:
2
divides lenWaa1
by PEPIN:22;
assume
y in rng IT
;
y in the_Edges_of Gthen 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;
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 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() ;
( 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;
for n being Element of NAT st 1 <= n & n <= len IT holds
IT . n Joins vs . n,vs . (n + 1),Glet n be
Element of
NAT ;
( 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
;
IT . n Joins vs . n,vs . (n + 1),Gset 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;
verum end;
then reconsider IT = IT as EdgeSeq of G by Def2;
take
IT
; ( 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; for n being Nat st 1 <= n & n <= len IT holds
IT . n = W . (2 * n)
let n be Nat; ( 1 <= n & n <= len IT implies IT . n = W . (2 * n) )
assume that
A18:
1 <= n
and
A19:
n <= len IT
; IT . n = W . (2 * n)
n in dom IT
by A18, A19, FINSEQ_3:25;
hence
IT . n = W . (2 * n)
by A1; verum