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); ( ( 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
; 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
hence
H = G
by FUNCT_2:12; verum