theorem :: BINARI_6:41

for A, Z being Element of Class EqBL2Nat
for n being Nat
for z being Element of BOOLEAN * st Z = Class (EqBL2Nat,z) & z = 0* n holds
( A + Z = A & Z + A = A )