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;
A7: the Sorts of (QuotMSAlg U1,(MSCng F)) . s = Class ((MSCng F) . s) by Def8
.= Class (MSCng F,s) by A1, Def20 ;
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
for x being set st x in the Sorts of (QuotMSAlg U1,(MSCng F)) . s holds
H . x = G . x

proof

let x be set ; :: thesis: ( x in the Sorts of (QuotMSAlg U1,(MSCng F)) . s implies H . x = G . x )
assume A10: 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 A7;
consider a being set such that
A11: ( a in the Sorts of U1 . s & x1 = Class (MSCng F,s),a ) by A7, A10, EQREL_1:def 5;
reconsider a = a as Element of the Sorts of U1 . s by A11;
thus H . x = (F . s) . a by A8, A11
.= G . x by A9, A11 ; :: thesis: verum

end;

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