for A1, A2 being object st A1 in Class EqBL2Nat & A2 in Class EqBL2Nat & QuBL2Nat . A1 = QuBL2Nat . A2 holds
A1 = A2
proof
let A1,
A2 be
object ;
( A1 in Class EqBL2Nat & A2 in Class EqBL2Nat & QuBL2Nat . A1 = QuBL2Nat . A2 implies A1 = A2 )
assume P0:
(
A1 in Class EqBL2Nat &
A2 in Class EqBL2Nat &
QuBL2Nat . A1 = QuBL2Nat . A2 )
;
A1 = A2
consider z1 being
object such that Q1:
(
z1 in BOOLEAN * &
A1 = Class (
EqBL2Nat,
z1) )
by P0, EQREL_1:def 3;
consider z2 being
object such that Q2:
(
z2 in BOOLEAN * &
A2 = Class (
EqBL2Nat,
z2) )
by P0, EQREL_1:def 3;
reconsider A10 =
A1,
A20 =
A2 as
Element of
Class EqBL2Nat by P0;
D1:
A10 is
Subset of
(BOOLEAN *)
by TARSKI:def 3;
D2:
A20 is
Subset of
(BOOLEAN *)
by TARSKI:def 3;
consider x1 being
object such that P1:
(
x1 in A10 &
QuBL2Nat . A10 = BL2Nat . x1 )
by Def400;
reconsider x1 =
x1 as
Element of
BOOLEAN * by D1, P1;
R1:
Class (
EqBL2Nat,
x1)
= Class (
EqBL2Nat,
z1)
by Q1, P1, EQREL_1:23;
consider x2 being
object such that P2:
(
x2 in A20 &
QuBL2Nat . A20 = BL2Nat . x2 )
by Def400;
reconsider x2 =
x2 as
Element of
BOOLEAN * by D2, P2;
R2:
Class (
EqBL2Nat,
x2)
= Class (
EqBL2Nat,
z2)
by Q2, P2, EQREL_1:23;
[x1,x2] in EqBL2Nat
by P1, P2, Def300, P0;
hence
A1 = A2
by EQREL_1:35, R1, R2, Q1, Q2;
verum
end;
hence
QuBL2Nat is one-to-one
by FUNCT_2:19; verum