let A, B be Element of Class EqBL2Nat; :: thesis: for x, y being Element of BOOLEAN * st x in A & y in B holds
A + B = Class (EqBL2Nat,(x + y))
let x2, y2 be Element of BOOLEAN * ; :: thesis: ( x2 in A & y2 in B implies A + B = Class (EqBL2Nat,(x2 + y2)) )
assume AS1: ( x2 in A & y2 in B ) ; :: thesis: A + B = Class (EqBL2Nat,(x2 + y2))
consider x1, y1 being Element of BOOLEAN * such that
T1: ( x1 in A & y1 in B & A + B = Class (EqBL2Nat,(x1 + y1)) ) by Def500;
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, AS1, T1, EQREL_1:22;
then R1: BL2Nat . x1 = BL2Nat . x2 by Def300;
[y1,y2] in EqBL2Nat by Q2, AS1, T1, 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 A + B = Class (EqBL2Nat,(x2 + y2)) by T1, EQREL_1:35; :: thesis: verum