theorem LM100: :: BINARI_6:29

for x, y being Element of NAT holds Nat2BL . (x + y) = (Nat2BL . x) + (Nat2BL . y)