let IT1, IT2 be FinSequence of NAT ; :: thesis: ( dom IT1 = dom (W .edgeSeq()) & ( for n being Nat st n in dom IT1 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT1 . 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 IT1 . n = EL . (W . (2 * n)) ) ) ) & dom IT2 = dom (W .edgeSeq()) & ( for n being Nat st n in dom IT2 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies IT2 . 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 IT2 . n = EL . (W . (2 * n)) ) ) ) implies IT1 = IT2 )
assume that
A12: dom IT1 = dom (W .edgeSeq()) and
A13: for n being Nat st n in dom IT1 holds
S1[n,IT1 . n] and
A14: dom IT2 = dom (W .edgeSeq()) and
A15: for n being Nat st n in dom IT2 holds
S1[n,IT2 . n] ; :: thesis: IT1 = IT2
now :: thesis: for n being Nat st n in dom IT1 holds
IT1 . n = IT2 . n
let n be Nat; :: thesis: ( n in dom IT1 implies IT1 . n = IT2 . n )
assume A16: n in dom IT1 ; :: thesis: IT1 . n = IT2 . n
now :: thesis: IT1 . n = IT2 . n
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 A17: W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G ; :: thesis: IT1 . n = IT2 . n
then IT1 . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) by A13, A16;
hence IT1 . n = IT2 . n by A12, A14, A15, A16, A17; :: thesis: verum
end;
suppose A18: not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G ; :: thesis: IT1 . n = IT2 . n
then IT1 . n = EL . (W . (2 * n)) by A13, A16;
hence IT1 . n = IT2 . n by A12, A14, A15, A16, A18; :: thesis: verum
end;
end;
end;
hence IT1 . n = IT2 . n ; :: thesis: verum
end;
hence IT1 = IT2 by A12, A14, FINSEQ_1:13; :: thesis: verum