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

proof

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

end;

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