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:
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:
A11: the Sorts of (QuotOSAlg (U1,(OSCng F))) . s = OSClass ((OSCng F),s) by Def11;
for x being object st x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s holds
H . x = G . x

let x be object ; :: thesis:
assume x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s ; :: thesis:
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, Def10;
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:

end;