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
;
ex b1 being Function of A,(QuotientOrder A) st
for x being Element of A holds b1 . x = Class ((EqRelOf A),x)defpred S1[
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) &
S1[
x,
y] )
proof
let x be
object ;
( x in the carrier of A implies ex y being object st
( y in the carrier of (QuotientOrder A) & S1[x,y] ) )
assume A3:
x in the
carrier of
A
;
ex y being object st
( y in the carrier of (QuotientOrder A) & S1[x,y] )
then reconsider z =
x as
Element of
A ;
set y =
Class (
(EqRelOf A),
z);
take
Class (
(EqRelOf A),
z)
;
( Class ((EqRelOf A),z) in the carrier of (QuotientOrder A) & S1[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;
S1[x, Class ((EqRelOf A),z)]
thus
S1[
x,
Class (
(EqRelOf A),
z)]
;
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
S1[
x,
f . x]
from FUNCT_2:sch 1(A2);
reconsider f =
f as
Function of
A,
(QuotientOrder A) ;
take
f
;
for x being Element of A holds f . x = Class ((EqRelOf A),x)let x be
Element of
A;
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;
verum end;