let f, g be Function of U1,(QuotUnivAlg U1,E); :: thesis: ( ( for u being Element of U1 holds f . u = Class E,u ) & ( for u being Element of U1 holds g . u = Class E,u ) implies f = g )
assume that
A3: for u being Element of U1 holds f . u = Class E,u and
A4: for u being Element of U1 holds g . u = Class E,u ; :: thesis: f = g

now

let u be Element of U1; :: thesis: f . u = g . u
f . u = Class E,u by A3;
hence f . u = g . u by A4; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum