defpred S₁[ 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 S₁[x,y]

proof

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

end;

consider f being Function of U1,(QuotUnivAlg U1,E) such that
A2: for x being Element of U1 holds S₁[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