theorem Th11: :: BINARI_4:11

for n being non zero Nat
for l, m being Nat st l + m <= (2 to_power n) - 1 holds
Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m