set RR = R quotient (E,F);
reconsider Q = Class F as a_partition of Y ;
now for e being object st e in Class E holds
e in dom (R quotient (E,F))let e be
object ;
( e in Class E implies e in dom (R quotient (E,F)) )reconsider ee =
e as
set by TARSKI:1;
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
object such that A1:
[x,y] in R
by XTUPLE_0:def 12;
reconsider yy =
y as
Element of
Y by ZFMISC_1:87, A1;
reconsider f =
EqClass (
yy,
Q) as
Element of
Class F ;
(
[e,f] = [e,f] &
x in ee &
y in f &
[x,y] in R )
by A1, EQREL_1:def 6;
then
[e,f] in R quotient (
E,
F)
;
hence
e in dom (R quotient (E,F))
by XTUPLE_0:def 12;
verum end;
then
Class E c= dom (R quotient (E,F))
by TARSKI:def 3;
hence
for b1 being Relation of (Class E),(Class F) st b1 = R quotient (E,F) holds
b1 is total
by PARTFUN1:def 2, XBOOLE_0:def 10; verum