reconsider lenWaa1 = (len W) - 1 as even Element of NAT by HEYTING3:1, INT_1:18;
set lenIT = lenWaa1 div 2;
reconsider lenIT = lenWaa1 div 2 as Element of NAT ;
2 divides lenWaa1
by PEPIN:22;
then A1:
lenWaa1 = 2 * lenIT
by NAT_D:3;
then A2:
len W = (2 * lenIT) + 1
;
deffunc H1( Nat) -> set = W . (2 * $1);
consider IT being FinSequence such that
A3:
( len IT = lenIT & ( for n being Nat st n in dom IT holds
IT . n = H1(n) ) )
from FINSEQ_1:sch 2();
now let y be
set ;
:: thesis: ( y in rng IT implies y in the_Edges_of G )assume
y in rng IT
;
:: thesis: y in the_Edges_of Gthen consider x being
set such that A4:
(
x in dom IT &
y = IT . x )
by FUNCT_1:def 5;
A5:
x in Seg lenIT
by A3, A4, FINSEQ_1:def 3;
reconsider x =
x as
Element of
NAT by A4;
A6:
y = W . (2 * x)
by A3, A4;
reconsider 2x = 2
* x as
even Element of
NAT ;
( 1
<= x &
x <= lenIT )
by A5, FINSEQ_1:3;
then A7:
( 1
* 2
<= 2
* x &
x * 2
<= lenIT * 2 )
by XREAL_1:66;
2
divides lenWaa1
by PEPIN:22;
then
2x <= lenWaa1
by A7, NAT_D:3;
then
2x + 1
<= lenWaa1 + 1
by XREAL_1:9;
then
(
2x <= 2x + 1 &
2x + 1
<= len W )
by NAT_1:11;
then A8:
2x <= len W
by XXREAL_0:2;
reconsider 2xaa1 =
2x - 1 as
odd Element of
NAT by A7, INT_1:18, XXREAL_0:2;
2xaa1 < len W
by A8, XREAL_1:149;
then
W . (2xaa1 + 1) Joins W . 2xaa1,
W . (2xaa1 + 2),
G
by Def3;
hence
y in the_Edges_of G
by A6, GLIB_000:def 15;
:: 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;
now 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 ) )A9:
((2 * (len IT)) + 1) + 1
= 2
* (len vs)
by A1, A3, Def14;
then A10:
2
* ((len IT) + 1) = 2
* (len vs)
;
thus
len vs = (len IT) + 1
by A9;
:: thesis: 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 ;
:: 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 A11:
( 1
<= n &
n <= len IT )
;
:: thesis: IT . n Joins vs . n,vs . (n + 1),Gthen A12:
( 1
<= n &
n <= len vs )
by A10, NAT_1:12;
A13:
( 1
<= n + 1 &
n + 1
<= len vs )
by A10, A11, NAT_1:12, XREAL_1:9;
set 2n = 2
* n;
reconsider 2n = 2
* n as
even Element of
NAT ;
set 2naa1 =
2n - 1;
1
<= n + n
by A11, NAT_1:12;
then reconsider 2naa1 =
2n - 1 as
odd Element of
NAT by INT_1:18;
A14:
(
vs . n = W . ((2 * n) - 1) &
vs . (n + 1) = W . ((2 * (n + 1)) - 1) )
by A12, A13, Def14;
n in dom IT
by A11, FINSEQ_3:27;
then A15:
IT . n = W . (2naa1 + 1)
by A3;
A16:
vs . (n + 1) = W . (2naa1 + 2)
by A14;
n * 2
<= (len IT) * 2
by A11, XREAL_1:66;
then
n * 2
<= len W
by A2, A3, NAT_1:12;
then
2naa1 < (len W) - 0
by XREAL_1:17;
hence
IT . n Joins vs . n,
vs . (n + 1),
G
by A14, A15, A16, 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 A1, A3; :: 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
( 1 <= n & n <= len IT )
; :: thesis: IT . n = W . (2 * n)
then
n in dom IT
by FINSEQ_3:27;
hence
IT . n = W . (2 * n)
by A3; :: thesis: verum