let IT1, IT2 be FinSequence of NAT ; ( 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]
; IT1 = IT2
now for n being Nat st n in dom IT1 holds
IT1 . n = IT2 . nlet n be
Nat;
( n in dom IT1 implies IT1 . n = IT2 . n )assume A16:
n in dom IT1
;
IT1 . n = IT2 . nhence
IT1 . n = IT2 . n
;
verum end;
hence
IT1 = IT2
by A12, A14, FINSEQ_1:13; verum