theorem :: BINARI_6:37

for A, B being Element of Class EqBL2Nat holds QuBL2Nat . (A + B) = (QuBL2Nat . A) + (QuBL2Nat . B)