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 :: thesis: for u being Element of U1 holds f . u = g . u

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 ; :: thesis: verum