set RR = R quotient (E,F);
reconsider Q = Class F as a_partition of Y ;
now let e be
set ;
( e in Class E implies e in dom (R quotient (E,F)) )assume
e in Class E
;
e in dom (R quotient (E,F))then reconsider ee =
e as
Element of
Class E ;
set xx = the
Element of
ee;
reconsider x = the
Element of
ee as
Element of
X ;
dom R = X
by PARTFUN1:def 2;
then consider y being
set such that C1:
[x,y] in R
by RELAT_1:def 4;
reconsider yy =
y as
Element of
Y by C1, ZFMISC_1:87;
reconsider f =
EqClass (
yy,
Q) as
Element of
Class F by EQREL_1:def 6;
(
[e,f] = [e,f] &
x in e &
y in f &
[x,y] in R )
by C1, EQREL_1:def 6;
then
[e,f] in R quotient (
E,
F)
;
hence
e in dom (R quotient (E,F))
by RELAT_1:def 4;
verum end;
then
Class E c= dom (R quotient (E,F))
by TARSKI:def 3;
then
Class E = dom (R quotient (E,F))
by XBOOLE_0:def 10;
hence
for b1 being Relation of (Class E),(Class F) st b1 = R quotient (E,F) holds
b1 is total
by PARTFUN1:def 2; verum