set qa = QuotOSAlg U1,R;
set cqa = the Sorts of (QuotOSAlg U1,R);
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
defpred S₁[ set , set ] means for a being Element of the Sorts of U1 . s st $1 = OSClass R,a holds
$2 = (F . s) . a;
A4: the Sorts of (QuotOSAlg U1,R) . s = OSClass R,s by Def13;
A5: for x being set st x in the Sorts of (QuotOSAlg U1,R) . s holds
ex y being set st
( y in the Sorts of U2 . s & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the Sorts of (QuotOSAlg U1,R) . s implies ex y being set st
( y in the Sorts of U2 . s & S₁[x,y] ) )
A6: R . s c= (OSCng F) . s by A3, PBOOLE:def 5;
assume x in the Sorts of (QuotOSAlg U1,R) . s ; :: thesis: ex y being set st
( y in the Sorts of U2 . s & S₁[x,y] )
then consider a being set such that
A7: a in the Sorts of U1 . s and
A8: x = Class (CompClass R,(CComp s)),a by A4, Def12;
reconsider a = a as Element of the Sorts of U1 . s by A7;
take y = (F . s) . a; :: thesis: ( y in the Sorts of U2 . s & S₁[x,y] )
thus y in the Sorts of U2 . s ; :: thesis: S₁[x,y]
let b be Element of the Sorts of U1 . s; :: thesis: ( x = OSClass R,b implies y = (F . s) . b )
assume A9: x = OSClass R,b ; :: thesis: y = (F . s) . b
x = OSClass R,a by A8;
then [b,a] in R . s by A9, Th13;
then [b,a] in (OSCng F) . s by A6;
then [b,a] in (MSCng F) . s by A1, A2, Def25;
then [b,a] in MSCng F,s by A1, MSUALG_4:def 20;
hence y = (F . s) . b by MSUALG_4:def 19; :: thesis: verum

end;

consider G being Function such that
A10: ( dom G = the Sorts of (QuotOSAlg U1,R) . s & rng G c= the Sorts of U2 . s & ( for x being set st x in the Sorts of (QuotOSAlg U1,R) . s holds
S₁[x,G . x] ) ) from WELLORD2:sch 1(A5);
reconsider G = G as Function of (the Sorts of (QuotOSAlg U1,R) . s),(the Sorts of U2 . s) by A10, FUNCT_2:def 1, RELSET_1:11;
take G ; :: thesis: for x being Element of the Sorts of U1 . s holds G . (OSClass R,x) = (F . s) . x
let a be Element of the Sorts of U1 . s; :: thesis: G . (OSClass R,a) = (F . s) . a
thus G . (OSClass R,a) = (F . s) . a by A4, A10; :: thesis: verum