let A, B be Element of Class EqBL2Nat; :: thesis: QuBL2Nat . (A + B) = (QuBL2Nat . A) + (QuBL2Nat . B)
P0: ( A in Class EqBL2Nat & B in Class EqBL2Nat ) ;
consider x being object such that
Q1: ( x in BOOLEAN * & A = Class (EqBL2Nat,x) ) by P0, EQREL_1:def 3;
consider y being object such that
Q2: ( y in BOOLEAN * & B = Class (EqBL2Nat,y) ) by P0, EQREL_1:def 3;
reconsider x = x, y = y as Element of BOOLEAN * by Q1, Q2;
( x in A & y in B ) by Q1, Q2, EQREL_1:20;
then A + B = Class (EqBL2Nat,(x + y)) by LM800;
then R2: QuBL2Nat . (A + B) = BL2Nat . (x + y) by LM700
.= (BL2Nat . x) + (BL2Nat . y) by LM240 ;
BL2Nat . x = QuBL2Nat . A by Q1, LM700;
hence QuBL2Nat . (A + B) = (QuBL2Nat . A) + (QuBL2Nat . B) by R2, Q2, LM700; :: thesis: verum