defpred S₁[ object , object ] means f . $1 = f . $2;
A1: for x being object st x in X holds
S₁[x,x] ;
A2: for x, y being object st S₁[x,y] holds
S₁[y,x] ;
A3: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z] ;
ex EqR being Equivalence_Relation of X st
for x, y being object holds
( [x,y] in EqR iff ( x in X & y in X & S₁[x,y] ) ) from EQREL_1:sch 1(A1, A2, A3);
hence ex b₁ being Equivalence_Relation of X st
for x, y being object holds
( [x,y] in b₁ iff ( x in X & y in X & f . x = f . y ) ) ; :: thesis: verum