theorem Th32: :: BINARI_4:32

for n being non zero Nat
for i being Integer
for j being Nat st 1 <= j & j <= n holds
(2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j