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₁[ object , object ] means for a being Element of the carrier of U1 st $1 = Class ((Cng f),a) holds
$2 = f . a;
A2: for x being object st x in the carrier of (QuotUnivAlg (U1,(Cng f))) holds
ex y being object st
( y in the carrier of U2 & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (QuotUnivAlg (U1,(Cng f))) implies ex y being object 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 object st
( y in the carrier of U2 & S₁[x,y] )
then reconsider x1 = x as Subset of the carrier of U1 ;
consider a being object such that
A4: a in the carrier of U1 and
A5: x1 = Class ((Cng f),a) by A3, EQREL_1:def 3;
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:23;
then [b,a] in Cng f by EQREL_1:19;
hence y = f . b by A1, Def12; :: 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 object st x in the carrier of (QuotUnivAlg (U1,(Cng f))) holds
S₁[x,F . x] ) ) from FUNCT_1:sch 6(A2);
reconsider F = F as Function of (QuotUnivAlg (U1,(Cng f))),U2 by A6, FUNCT_2:def 1, RELSET_1:4;
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 3;
hence F . (Class ((Cng f),a)) = f . a by A6; :: thesis: verum