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