set qa = QuotientOrder A;

set car = the carrier of A;

set carq = the carrier of (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 )
;

end;

suppose A1:
not A is empty
; :: thesis: ex b_{1} being Function of A,(QuotientOrder A) st

for x being Element of A holds b_{1} . x = Class ((EqRelOf A),x)

for x being Element of A holds b

defpred S_{1}[ 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_{1}[x,y] )

A4: for x being object st x in the carrier of A holds

S_{1}[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;( $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

proof

consider f being Function of the carrier of A, the carrier of (QuotientOrder A) such that
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_{1}[x,y] ) )

assume A3: x in the carrier of A ; :: thesis: ex y being object st

( y in the carrier of (QuotientOrder A) & S_{1}[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_{1}[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_{1}[x, Class ((EqRelOf A),z)]

thus S_{1}[x, Class ((EqRelOf A),z)]
; :: thesis: verum

end;( y in the carrier of (QuotientOrder A) & S

assume A3: x in the carrier of A ; :: thesis: ex y being object st

( y in the carrier of (QuotientOrder A) & S

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

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

thus S

A4: for x being object st x in the carrier of A holds

S

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

suppose A6:
A is empty
; :: thesis: ex b_{1} being Function of A,(QuotientOrder A) st

for x being Element of A holds b_{1} . x = Class ((EqRelOf A),x)

for x being Element of A holds b

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;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