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 8 :: 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 object such that
A9: ( a in the carrier of U1 & x1 = Class ((Cng f),a) ) by EQREL_1:def 3;
thus F . x = f . a by A7, A9
.= G . x by A8, A9 ; :: thesis: verum