set RR = R quotient (E,F);

reconsider Q = Class F as a_partition of Y ;

hence for b_{1} being Relation of (Class E),(Class F) st b_{1} = R quotient (E,F) holds

b_{1} is total
by PARTFUN1:def 2, XBOOLE_0:def 10; :: thesis: verum

reconsider Q = Class F as a_partition of Y ;

now :: thesis: for e being object st e in Class E holds

e in dom (R quotient (E,F))

then
Class E c= dom (R quotient (E,F))
by TARSKI:def 3;e in dom (R quotient (E,F))

let e be object ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;reconsider ee = e as set by TARSKI:1;

assume e in Class E ; :: thesis: 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; :: thesis: verum

hence for b

b