now :: thesis: for k being Nat st k in Seg (len (W .edgeSeq())) holds
ex x being object st S1[k,x]
let k be Nat; :: thesis: ( k in Seg (len (W .edgeSeq())) implies ex x being object st S1[k,x] )
assume k in Seg (len (W .edgeSeq())) ; :: thesis: ex x being object st S1[k,x]
now :: thesis: 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 ; :: thesis: ex x being set st S1[k,x]
hence ex x being set st S1[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 S1[k,x]
hence ex x being set st S1[k,x] ; :: thesis: verum
end;
end;
end;
hence ex x being object st S1[k,x] ; :: thesis: 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 :: thesis: for y being object st y in rng IT holds
y in NAT
let y be object ; :: thesis: ( y in rng IT implies b1 in NAT )
assume y in rng IT ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G ; :: thesis: b1 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