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; ( ( 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
; F = G
let x be Element of the carrier of (QuotUnivAlg (U1,(Cng f))); FUNCT_2:def 8 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
; verum