now

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

now

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

end;

then A2: for k being Nat st k in Seg (len (W .edgeSeq() )) holds
ex x being set st S₁[k,x] ;
consider IT being FinSequence such that
A3: dom IT = Seg (len (W .edgeSeq() )) and
A3a: for k being Nat st k in Seg (len (W .edgeSeq() )) holds
S₁[k,IT . k] from FINSEQ_1:sch 1(A2);

now

let y be set ; :: thesis: ( y in rng IT implies b₁ in NAT )
assume y in rng IT ; :: thesis: b₁ in NAT
then consider x being set such that
A4: ( x in dom IT & IT . x = y ) by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A4;

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 S1: W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G ; :: thesis: b₁ in NAT

n in dom (W .edgeSeq() ) by A3, A4, FINSEQ_1:def 3;
then 2 * n in dom W by GLIB_001:79;
then A2c: ( 1 <= 2 * n & 2 * n <= len W ) by FINSEQ_3:27;
then reconsider 2n1 = (2 * n) - 1 as odd Element of NAT by INT_1:18;
A3c: 2n1 < (len W) - 0 by A2c, XREAL_1:17;
A4c: 2n1 + 1 = 2 * n ;
A5c: 2n1 + (1 + 1) = (2 * n) + 1 ;
B1: IT . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) by S1, A4, A3, A3a;
EL . (W . (2 * n)) < (the_Weight_of G) . (W . (2 * n)) by A, S1, A3c, A4c, A5c, Def12;
hence y in NAT by A4, B1, INT_1:18; :: 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 A4, A3, A3a;
hence y in NAT by A4, ORDINAL1:def 13; :: thesis: verum

end;

end;

end;

then rng IT c= NAT by TARSKI:def 3;
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, A3a; :: thesis: verum