now :: thesis: for k being Nat st k in Seg (len (W .edgeSeq())) holds
ex x being object st S₁[k,x]

let k be Nat; :: thesis: ( k in Seg (len (W .edgeSeq())) implies ex x being object st S₁[k,x] )
assume k in Seg (len (W .edgeSeq())) ; :: thesis: ex x being object st S₁[k,x]

now :: thesis: ex x being set st S₁[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 ; :: thesis: ex x being set st S₁[k,x]

hence ex x being set st S₁[k,x] ; :: thesis: verum

end;

suppose not W . (2 * k) DJoins W . ((2 * k) - 1),W . ((2 * k) + 1),G ; :: thesis: ex x being set st S₁[k,x]

hence ex x being set st S₁[k,x] ; :: thesis: verum

end;

end;

end;

hence ex x being object st S₁[k,x] ; :: thesis: verum

end;

then A2: for k being Nat st k in Seg (len (W .edgeSeq())) holds
ex x being object st S₁[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
S₁[k,IT . k] from FINSEQ_1:sch 1(A2);

now :: thesis: for y being object st y in rng IT holds
y in NAT

let y be object ; :: thesis: ( y in rng IT implies b₁ in NAT )
assume y in rng IT ; :: thesis: b₁ 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 ; :: thesis: b₁ 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; :: thesis: verum

end;

suppose not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G ; :: thesis: b₁ in NAT

then IT . n = EL . (W . (2 * n)) by A3, A4, A5;
hence y in NAT by A6, ORDINAL1:def 12; :: thesis: verum

end;

end;

end;

then rng IT c= NAT ;
then reconsider IT = IT as FinSequence of NAT by FINSEQ_1:def 4;
take IT ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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; :: thesis: verum