set qa = QuotOSAlg (U1,R);
set cqa = the Sorts of (QuotOSAlg (U1,R));
set u1 = the Sorts of U1;
set u2 = the Sorts of U2;
let H, G be Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s); :: thesis: ( ( for x being Element of the Sorts of U1 . s holds H . (OSClass (R,x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds G . (OSClass (R,x)) = (F . s) . x ) implies H = G )
assume that
A11: for a being Element of the Sorts of U1 . s holds H . (OSClass (R,a)) = (F . s) . a and
A12: for a being Element of the Sorts of U1 . s holds G . (OSClass (R,a)) = (F . s) . a ; :: thesis: H = G
A13: the Sorts of (QuotOSAlg (U1,R)) . s = OSClass (R,s) by Def11;
for x being object st x in the Sorts of (QuotOSAlg (U1,R)) . s holds
H . x = G . x

proof

let x be object ; :: thesis: ( x in the Sorts of (QuotOSAlg (U1,R)) . s implies H . x = G . x )
assume x in the Sorts of (QuotOSAlg (U1,R)) . s ; :: thesis: H . x = G . x
then consider y being set such that
A14: y in the Sorts of U1 . s and
A15: x = Class ((CompClass (R,(CComp s))),y) by A13, Def10;
reconsider y1 = y as Element of the Sorts of U1 . s by A14;
A16: OSClass (R,y1) = x by A15;
hence H . x = (F . s) . y1 by A11
.= G . x by A12, A16 ;
:: thesis: verum

end;

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