theorem Th7: :: BINARI_2:7

for m being non zero Nat holds Bin1 (m + 1) = (Bin1 m) ^ <*FALSE*>