theorem Th14: :: BINARI_4:14

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