set qa = QuotientOrder A;
set car = the carrier of A;
set carq = the carrier of ();
per cases ( not A is empty or A is empty ) ;
suppose A1: not A is empty ; :: thesis: ex b1 being Function of A,() st
for x being Element of A holds b1 . x = Class ((),x)

defpred S1[ object , object ] means ex z being Element of A st
( \$1 = z & \$2 = Class ((),z) );
A2: for x being object st x in the carrier of A holds
ex y being object st
( y in the carrier of () & S1[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 () & S1[x,y] ) )

assume A3: x in the carrier of A ; :: thesis: ex y being object st
( y in the carrier of () & S1[x,y] )

then reconsider z = x as Element of A ;
set y = Class ((),z);
take Class ((),z) ; :: thesis: ( Class ((),z) in the carrier of () & S1[x, Class ((),z)] )
Class ((),z) in Class () by ;
hence Class ((),z) in the carrier of () by Def7; :: thesis: S1[x, Class ((),z)]
thus S1[x, Class ((),z)] ; :: thesis: verum
end;
consider f being Function of the carrier of A, the carrier of () such that
A4: for x being object st x in the carrier of A holds
S1[x,f . x] from reconsider f = f as Function of A,() ;
take f ; :: thesis: for x being Element of A holds f . x = Class ((),x)
let x be Element of A; :: thesis: f . x = Class ((),x)
consider z being Element of A such that
A5: ( x = z & f . x = Class ((),z) ) by A4, A1;
thus f . x = Class ((),x) by A5; :: thesis: verum
end;
suppose A6: A is empty ; :: thesis: ex b1 being Function of A,() st
for x being Element of A holds b1 . x = Class ((),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 () by FUNCT_1:8;
reconsider f = f as Function of the carrier of A, the carrier of () by ;
reconsider f = f as Function of A,() ;
take f ; :: thesis: for x being Element of A holds f . x = Class ((),x)
A9: for x being Element of A holds Class ((),x) = {} by A6;
let x be Element of A; :: thesis: f . x = Class ((),x)
thus f . x = {} by A6
.= Class ((),x) by A9 ; :: thesis: verum
end;
end;