defpred S₁[ object , object ] means (F . s) . $1 = (F . s) . $2;
set S1 = the Sorts of U1 . s;
A1: for x, y being object st S₁[x,y] holds
S₁[y,x] ;
A2: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z] ;
A3: for x being object st x in the Sorts of U1 . s holds
S₁[x,x] ;
consider R being Equivalence_Relation of ( the Sorts of U1 . s) such that
A4: for x, y being object holds
( [x,y] in R iff ( x in the Sorts of U1 . s & y in the Sorts of U1 . s & S₁[x,y] ) ) from EQREL_1:sch 1(A3, A1, A2);
take R ; :: thesis: for x, y being Element of the Sorts of U1 . s holds
( [x,y] in R iff (F . s) . x = (F . s) . y )
let x, y be Element of the Sorts of U1 . s; :: thesis: ( [x,y] in R iff (F . s) . x = (F . s) . y )
thus ( [x,y] in R iff (F . s) . x = (F . s) . y ) by A4; :: thesis: verum