now for k being Nat st k in Seg (len (W .edgeSeq())) holds
ex x being object st S1[k,x]let k be
Nat;
( k in Seg (len (W .edgeSeq())) implies ex x being object st S1[k,x] )assume
k in Seg (len (W .edgeSeq()))
;
ex x being object st S1[k,x]now ex x being set st S1[k,x]per cases
( W . (2 * k) DJoins W . ((2 * k) - 1),W . ((2 * k) + 1),G or not W . (2 * k) DJoins W . ((2 * k) - 1),W . ((2 * k) + 1),G )
;
suppose
W . (2 * k) DJoins W . ((2 * k) - 1),
W . ((2 * k) + 1),
G
;
ex x being set st S1[k,x]hence
ex
x being
set st
S1[
k,
x]
;
verum end; suppose
not
W . (2 * k) DJoins W . ((2 * k) - 1),
W . ((2 * k) + 1),
G
;
ex x being set st S1[k,x]hence
ex
x being
set st
S1[
k,
x]
;
verum end; end; end; hence
ex
x being
object st
S1[
k,
x]
;
verum end;
then A2:
for k being Nat st k in Seg (len (W .edgeSeq())) holds
ex x being object st S1[k,x]
;
consider IT being FinSequence such that
A3:
dom IT = Seg (len (W .edgeSeq()))
and
A4:
for k being Nat st k in Seg (len (W .edgeSeq())) holds
S1[k,IT . k]
from FINSEQ_1:sch 1(A2);
now for y being object st y in rng IT holds
y in NAT let y be
object ;
( y in rng IT implies b1 in NAT )assume
y in rng IT
;
b1 in NAT then consider x being
object such that A5:
x in dom IT
and A6:
IT . x = y
by FUNCT_1:def 3;
reconsider n =
x as
Element of
NAT by A5;
per cases
( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G or not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G )
;
suppose A7:
W . (2 * n) DJoins W . ((2 * n) - 1),
W . ((2 * n) + 1),
G
;
b1 in NAT
n in dom (W .edgeSeq())
by A3, A5, FINSEQ_1:def 3;
then A8:
2
* n in dom W
by GLIB_001:78;
then
1
<= 2
* n
by FINSEQ_3:25;
then reconsider 2n1 =
(2 * n) - 1 as
odd Element of
NAT by INT_1:5;
2
* n <= len W
by A8, FINSEQ_3:25;
then A9:
2n1 < (len W) - 0
by XREAL_1:15;
A10:
2n1 + (1 + 1) = (2 * n) + 1
;
A11:
IT . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n)))
by A3, A4, A5, A7;
2n1 + 1
= 2
* n
;
then
EL . (W . (2 * n)) < (the_Weight_of G) . (W . (2 * n))
by A1, A7, A9, A10;
hence
y in NAT
by A6, A11, INT_1:5;
verum end; end; end;
then
rng IT c= NAT
;
then reconsider IT = IT as FinSequence of NAT by FINSEQ_1:def 4;
take
IT
; ( dom IT = dom (W .edgeSeq()) & ( for n being Nat st n in dom IT holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = EL . (W . (2 * n)) ) ) ) )
thus
dom IT = dom (W .edgeSeq())
by A3, FINSEQ_1:def 3; for n being Nat st n in dom IT holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = EL . (W . (2 * n)) ) )
let n be Nat; ( n in dom IT implies ( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = EL . (W . (2 * n)) ) ) )
assume
n in dom IT
; ( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = EL . (W . (2 * n)) ) )
hence
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT . n = EL . (W . (2 * n)) ) )
by A3, A4; verum