defpred S₁[ object , object ] means $1 = $2;
for f, g being Function of [:A,A:],BOOLEAN st ( for x, y being object st x in A & y in A holds
( ( S₁[x,y] implies f . (x,y) = TRUE ) & ( not S₁[x,y] implies f . (x,y) = FALSE ) ) ) & ( for x, y being object st x in A & y in A holds
( ( S₁[x,y] implies g . (x,y) = TRUE ) & ( not S₁[x,y] implies g . (x,y) = FALSE ) ) ) holds
f = g from NOMIN_4:sch 2();
hence for b₁, b₂ being Function of [:A,A:],BOOLEAN st ( for a, b being object st a in A & b in A holds
( ( a = b implies b₁ . (a,b) = TRUE ) & ( a <> b implies b₁ . (a,b) = FALSE ) ) ) & ( for a, b being object st a in A & b in A holds
( ( a = b implies b₂ . (a,b) = TRUE ) & ( a <> b implies b₂ . (a,b) = FALSE ) ) ) holds
b₁ = b₂ ; :: thesis: verum