set qa = QuotientOrder A;
set car = the carrier of A;
set carq = the carrier of (QuotientOrder A);

per cases ( not A is empty or A is empty ) ;

suppose A1: not A is empty ; :: thesis: ex b₁ being Function of A,(QuotientOrder A) st
for x being Element of A holds b₁ . x = Class ((EqRelOf A),x)

defpred S₁[ object , object ] means ex z being Element of A st
( $1 = z & $2 = Class ((EqRelOf A),z) );
A2: for x being object st x in the carrier of A holds
ex y being object st
( y in the carrier of (QuotientOrder A) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of A implies ex y being object st
( y in the carrier of (QuotientOrder A) & S₁[x,y] ) )
assume A3: x in the carrier of A ; :: thesis: ex y being object st
( y in the carrier of (QuotientOrder A) & S₁[x,y] )
then reconsider z = x as Element of A ;
set y = Class ((EqRelOf A),z);
take Class ((EqRelOf A),z) ; :: thesis: ( Class ((EqRelOf A),z) in the carrier of (QuotientOrder A) & S₁[x, Class ((EqRelOf A),z)] )
Class ((EqRelOf A),z) in Class (EqRelOf A) by A3, EQREL_1:def 3;
hence Class ((EqRelOf A),z) in the carrier of (QuotientOrder A) by Def7; :: thesis: S₁[x, Class ((EqRelOf A),z)]
thus S₁[x, Class ((EqRelOf A),z)] ; :: thesis: verum

end;

consider f being Function of the carrier of A, the carrier of (QuotientOrder A) such that
A4: for x being object st x in the carrier of A holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
reconsider f = f as Function of A,(QuotientOrder A) ;
take f ; :: thesis: for x being Element of A holds f . x = Class ((EqRelOf A),x)
let x be Element of A; :: thesis: f . x = Class ((EqRelOf A),x)
consider z being Element of A such that
A5: ( x = z & f . x = Class ((EqRelOf A),z) ) by A4, A1;
thus f . x = Class ((EqRelOf A),x) by A5; :: thesis: verum

end;

suppose A6: A is empty ; :: thesis: ex b₁ being Function of A,(QuotientOrder A) st
for x being Element of A holds b₁ . x = Class ((EqRelOf A),x)

then the carrier of A = {} ;
then consider f being Function such that
A7: the carrier of A = dom f and
A8: rng f c= the carrier of (QuotientOrder A) by FUNCT_1:8;
reconsider f = f as Function of the carrier of A, the carrier of (QuotientOrder A) by A7, A8, FUNCT_2:2;
reconsider f = f as Function of A,(QuotientOrder A) ;
take f ; :: thesis: for x being Element of A holds f . x = Class ((EqRelOf A),x)
A9: for x being Element of A holds Class ((EqRelOf A),x) = {} by A6;
let x be Element of A; :: thesis: f . x = Class ((EqRelOf A),x)
thus f . x = {} by A6
.= Class ((EqRelOf A),x) by A9 ; :: thesis: verum

end;

end;