defpred S1[ Element of U1, set ] means $2 = Class (E,$1);
A1: for x being Element of U1 ex y being Element of (QuotUnivAlg (U1,E)) st S1[x,y]
proof
let x be Element of U1; :: thesis: ex y being Element of (QuotUnivAlg (U1,E)) st S1[x,y]
reconsider y = Class (E,x) as Element of (QuotUnivAlg (U1,E)) by EQREL_1:def 3;
take y ; :: thesis: S1[x,y]
thus S1[x,y] ; :: thesis: verum
end;
consider f being Function of U1,(QuotUnivAlg (U1,E)) such that
A2: for x being Element of U1 holds S1[x,f . x] from FUNCT_2:sch 3(A1);
 take f ; :: thesis: for u being Element of U1 holds f . u = Class (E,u)
thus for u being Element of U1 holds f . u = Class (E,u) by A2; :: thesis: verum