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
A3: for x being Element of X holds S₁[x,f . x] from FUNCT_2:sch 3(A1);

now

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

end;

then reconsider f = f as BCI-homomorphism of X,(X ./. RI) by Def0;
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 A3; :: thesis: verum