set qa = QuotMSAlg (U1,(MSCng F));
set cqa = the Sorts of (QuotMSAlg (U1,(MSCng F)));
set u1 = the Sorts of U1;
set u2 = the Sorts of U2;
let H, G be Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s); :: thesis: ( ( for x being Element of the Sorts of U1 . s holds H . (Class ((MSCng (F,s)),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds G . (Class ((MSCng (F,s)),x)) = (F . s) . x ) implies H = G )
assume that
A8: for a being Element of the Sorts of U1 . s holds H . (Class ((MSCng (F,s)),a)) = (F . s) . a and
A9: for a being Element of the Sorts of U1 . s holds G . (Class ((MSCng (F,s)),a)) = (F . s) . a ; :: thesis: H = G
A10: the Sorts of (QuotMSAlg (U1,(MSCng F))) . s = Class ((MSCng F) . s) by Def6
.= Class (MSCng (F,s)) by A1, Def18 ;
for x being object st x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s holds
H . x = G . x

proof

let x be object ; :: thesis: ( x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s implies H . x = G . x )
assume A11: x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s ; :: thesis: H . x = G . x
then reconsider x1 = x as Subset of ( the Sorts of U1 . s) by A10;
consider a being object such that
A12: a in the Sorts of U1 . s and
A13: x1 = Class ((MSCng (F,s)),a) by A10, A11, EQREL_1:def 3;
reconsider a = a as Element of the Sorts of U1 . s by A12;
thus H . x = (F . s) . a by A8, A13
.= G . x by A9, A13 ; :: thesis: verum

end;

hence H = G by FUNCT_2:12; :: thesis: verum