set qa = QuotMSAlg (U1,(MSCng F));
set cqa = the Sorts of (QuotMSAlg (U1,(MSCng F)));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
defpred S₁[ object , object ] means for a being Element of the Sorts of U1 . s st $1 = Class ((MSCng (F,s)),a) holds
$2 = (F . s) . a;
A2: the Sorts of (QuotMSAlg (U1,(MSCng F))) . s = Class ((MSCng F) . s) by Def6
.= Class (MSCng (F,s)) by A1, Def18 ;
A3: for x being object st x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s holds
ex y being object st
( y in the Sorts of U2 . s & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s implies ex y being object st
( y in the Sorts of U2 . s & S₁[x,y] ) )
assume A4: x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s ; :: thesis: ex y being object st
( y in the Sorts of U2 . s & S₁[x,y] )
then reconsider x1 = x as Subset of ( the Sorts of U1 . s) by A2;
consider a being object such that
A5: a in the Sorts of U1 . s and
A6: x1 = Class ((MSCng (F,s)),a) by A2, A4, EQREL_1:def 3;
reconsider a = a as Element of the Sorts of U1 . s by A5;
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 = Class ((MSCng (F,s)),b) implies y = (F . s) . b )
assume x = Class ((MSCng (F,s)),b) ; :: thesis: y = (F . s) . b
then b in Class ((MSCng (F,s)),a) by A6, EQREL_1:23;
then [b,a] in MSCng (F,s) by EQREL_1:19;
hence y = (F . s) . b by Def17; :: thesis: verum

end;

consider G being Function such that
A7: ( dom G = the Sorts of (QuotMSAlg (U1,(MSCng F))) . s & rng G c= the Sorts of U2 . s & ( for x being object st x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s holds
S₁[x,G . x] ) ) from FUNCT_1:sch 6(A3);
reconsider G = G as Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) by A7, FUNCT_2:def 1, RELSET_1:4;
take G ; :: thesis: for x being Element of the Sorts of U1 . s holds G . (Class ((MSCng (F,s)),x)) = (F . s) . x
let a be Element of the Sorts of U1 . s; :: thesis: G . (Class ((MSCng (F,s)),a)) = (F . s) . a
Class ((MSCng (F,s)),a) in Class (MSCng (F,s)) by EQREL_1:def 3;
hence G . (Class ((MSCng (F,s)),a)) = (F . s) . a by A2, A7; :: thesis: verum