set qa = QuotUnivAlg U1,(Cng f);
set cqa = the carrier of (QuotUnivAlg U1,(Cng f));
set u1 = the carrier of U1;
set u2 = the carrier of U2;
defpred S₁[ set , set ] means for a being Element of the carrier of U1 st $1 = Class (Cng f),a holds
$2 = f . a;
A2: for x being set st x in the carrier of (QuotUnivAlg U1,(Cng f)) holds
ex y being set st
( y in the carrier of U2 & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the carrier of (QuotUnivAlg U1,(Cng f)) implies ex y being set st
( y in the carrier of U2 & S₁[x,y] ) )
assume A3: x in the carrier of (QuotUnivAlg U1,(Cng f)) ; :: thesis: ex y being set st
( y in the carrier of U2 & S₁[x,y] )
then reconsider x1 = x as Subset of the carrier of U1 ;
consider a being set such that
A4: a in the carrier of U1 and
A5: x1 = Class (Cng f),a by A3, EQREL_1:def 5;
reconsider a = a as Element of the carrier of U1 by A4;
take y = f . a; :: thesis: ( y in the carrier of U2 & S₁[x,y] )
thus y in the carrier of U2 ; :: thesis: S₁[x,y]
let b be Element of the carrier of U1; :: thesis: ( x = Class (Cng f),b implies y = f . b )
assume x = Class (Cng f),b ; :: thesis: y = f . b
then b in Class (Cng f),a by A5, EQREL_1:31;
then [b,a] in Cng f by EQREL_1:27;
hence y = f . b by A1, Def16; :: thesis: verum

end;

consider F being Function such that
A6: ( dom F = the carrier of (QuotUnivAlg U1,(Cng f)) & rng F c= the carrier of U2 & ( for x being set st x in the carrier of (QuotUnivAlg U1,(Cng f)) holds
S₁[x,F . x] ) ) from WELLORD2:sch 1(A2);
reconsider F = F as Function of (QuotUnivAlg U1,(Cng f)),U2 by A6, FUNCT_2:def 1, RELSET_1:11;
take F ; :: thesis: for a being Element of U1 holds F . (Class (Cng f),a) = f . a
let a be Element of the carrier of U1; :: thesis: F . (Class (Cng f),a) = f . a
Class (Cng f),a in Class (Cng f) by EQREL_1:def 5;
hence F . (Class (Cng f),a) = f . a by A6; :: thesis: verum