:: deftheorem defines are_different_wrt NOMIN_7:def 2 :
for V being set
for loc being b₁ -valued Function
for val being Function
for N being Nat holds
( loc,val are_different_wrt N iff for m, n being Nat st 1 <= m & m <= N & 1 <= n & n <= N holds
val . m <> loc /. n );