set qa = QuotUnivAlg U1,(Cng f);
set cqa = the carrier of (QuotUnivAlg U1,(Cng f));
set u1 = the carrier of U1;
let F, G be Function of (QuotUnivAlg U1,(Cng f)),U2; :: thesis: ( ( for a being Element of U1 holds F . (Class (Cng f),a) = f . a ) & ( for a being Element of U1 holds G . (Class (Cng f),a) = f . a ) implies F = G )
assume that
A7: for a being Element of the carrier of U1 holds F . (Class (Cng f),a) = f . a and
A8: for a being Element of the carrier of U1 holds G . (Class (Cng f),a) = f . a ; :: thesis: F = G
let x be Element of the carrier of (QuotUnivAlg U1,(Cng f)); :: according to FUNCT_2:def 9 :: thesis: F . x = G . x
x in the carrier of (QuotUnivAlg U1,(Cng f)) ;
then reconsider x1 = x as Subset of the carrier of U1 ;
consider a being set such that
A9: ( a in the carrier of U1 & x1 = Class (Cng f),a ) by EQREL_1:def 5;
thus F . x = f . a by A7, A9
.= G . x by A8, A9 ; :: thesis: verum