for k being Nat
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S st I is ins-loc-free holds
IncAddr (I,k) = I