let AB1, AB2 be Element of Class EqBL2Nat; :: thesis: ( ex x, y being Element of BOOLEAN * st
( x in A & y in B & AB1 = Class (EqBL2Nat,(x + y)) ) & ex x, y being Element of BOOLEAN * st
( x in A & y in B & AB2 = Class (EqBL2Nat,(x + y)) ) implies AB1 = AB2 )
assume that
P1: ex x, y being Element of BOOLEAN * st
( x in A & y in B & AB1 = Class (EqBL2Nat,(x + y)) ) and
P2: ex x, y being Element of BOOLEAN * st
( x in A & y in B & AB2 = Class (EqBL2Nat,(x + y)) ) ; :: thesis: AB1 = AB2
consider x1, y1 being Element of BOOLEAN * such that
P3: ( x1 in A & y1 in B & AB1 = Class (EqBL2Nat,(x1 + y1)) ) by P1;
consider x2, y2 being Element of BOOLEAN * such that
P4: ( x2 in A & y2 in B & AB2 = Class (EqBL2Nat,(x2 + y2)) ) by P2;
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;
[x1,x2] in EqBL2Nat by Q1, P3, P4, EQREL_1:22;
then R1: BL2Nat . x1 = BL2Nat . x2 by Def300;
[y1,y2] in EqBL2Nat by Q2, P3, P4, EQREL_1:22;
then R2: BL2Nat . y1 = BL2Nat . y2 by Def300;
BL2Nat . (x1 + y1) = (BL2Nat . x1) + (BL2Nat . y1) by LM240
.= BL2Nat . (x2 + y2) by LM240, R1, R2 ;
then [(x1 + y1),(x2 + y2)] in EqBL2Nat by Def300;
hence AB1 = AB2 by P3, P4, EQREL_1:35; :: thesis: verum