defpred S₁[ Element of X, set ] means $2 = Class RI,$1;
A1: for x being Element of X ex y being Element of (X ./. RI) st S₁[x,y]

proof

let x be Element of X; :: thesis: ex y being Element of (X ./. RI) st S₁[x,y]
reconsider y = Class RI,x as Element of (X ./. RI) by EQREL_1:def 5;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function of X,(X ./. RI) such that
A2: for x being Element of X holds S₁[x,f . x] from FUNCT_2:sch 3(A1);

now

reconsider E = RI as Congruence of X ;
let a, b be Element of X; :: thesis: (f . a) \ (f . b) = f . (a \ b)
reconsider w1 = Class E,a, w2 = Class E,b as Element of (X ./. RI) by EQREL_1:def 5;
( f . a = Class RI,a & f . b = Class RI,b ) by A2;
then (f . a) \ (f . b) = Class RI,(a \ b) by BCIALG_2:def 17;
hence (f . a) \ (f . b) = f . (a \ b) by A2; :: thesis: verum

end;

then reconsider f = f as BCI-homomorphism of X,(X ./. RI) by Def6;
take f ; :: thesis: for x being Element of X holds f . x = Class RI,x
thus for x being Element of X holds f . x = Class RI,x by A2; :: thesis: verum