let f1, f2 be Function of (Class EqBL2Nat),NAT; :: thesis: ( ( for A being Element of Class EqBL2Nat ex x being object st
( x in A & f1 . A = BL2Nat . x ) ) & ( for A being Element of Class EqBL2Nat ex x being object st
( x in A & f2 . A = BL2Nat . x ) ) implies f1 = f2 )
assume AS1: for A being Element of Class EqBL2Nat ex x being object st
( x in A & f1 . A = BL2Nat . x ) ; :: thesis: ( ex A being Element of Class EqBL2Nat st
for x being object holds
( not x in A or not f2 . A = BL2Nat . x ) or f1 = f2 )
assume AS2: for A being Element of Class EqBL2Nat ex x being object st
( x in A & f2 . A = BL2Nat . x ) ; :: thesis: f1 = f2
for A being Element of Class EqBL2Nat holds f1 . A = f2 . A
proof
let A be Element of Class EqBL2Nat; :: thesis: f1 . A = f2 . A
consider x1 being object such that
P1: ( x1 in A & f1 . A = BL2Nat . x1 ) by AS1;
consider x2 being object such that
P2: ( x2 in A & f2 . A = BL2Nat . x2 ) by AS2;
A is Subset of (BOOLEAN *) by TARSKI:def 3;
then consider x being object such that
P3: ( x in BOOLEAN * & A = Class (EqBL2Nat,x) ) by EQREL_1:def 3;
[x1,x2] in EqBL2Nat by EQREL_1:22, P1, P2, P3;
hence f1 . A = f2 . A by P1, P2, Def300; :: thesis: verum
end;
hence f1 = f2 by FUNCT_2:def 8; :: thesis: verum