let AB1, AB2 be Element of Class EqBL2Nat; ( 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)) )
; 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; verum