theorem LM240: :: BINARI_6:34

for x, y being Element of BOOLEAN * holds BL2Nat . (x + y) = (BL2Nat . x) + (BL2Nat . y)