theorem Th1: :: NOMIN_7:1

for N being Nat
for V being set
for loc being b₂ -valued Function st loc | (Seg N) is one-to-one & Seg N c= dom loc holds
for i, j being Nat st 1 <= i & i <= N & 1 <= j & j <= N & i <> j holds
loc /. i <> loc /. j