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 3;
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 :: thesis: for a, b being Element of X holds (f . a) \ (f . b) = f . (a \ b)

let a, b be Element of X; :: thesis: (f . a) \ (f . b) = f . (a \ b)
( 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