let EqR1, EqR2 be Equivalence_Relation of (BOOLEAN *); :: thesis: ( ( for x, y being object holds
( [x,y] in EqR1 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) & ( for x, y being object holds
( [x,y] in EqR2 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) implies EqR1 = EqR2 )
assume that
A1: for x, y being object holds
( [x,y] in EqR1 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) and
A2: for x, y being object holds
( [x,y] in EqR2 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ; :: thesis: EqR1 = EqR2
for a, b being object holds
( [a,b] in EqR1 iff [a,b] in EqR2 )

proof

let x, y be object ; :: thesis: ( [x,y] in EqR1 iff [x,y] in EqR2 )
( [x,y] in EqR1 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) by A1;
hence ( [x,y] in EqR1 iff [x,y] in EqR2 ) by A2; :: thesis: verum

end;

hence EqR1 = EqR2 ; :: thesis: verum