set IT = f quotient (E,F);

reconsider P = Class E as a_partition of X ;

reconsider EEE = E as Relation of X,X ;

_{1} being Relation st b_{1} = f quotient (E,F) holds

b_{1} is Function-like
by FUNCT_1:def 1; :: thesis: verum

reconsider P = Class E as a_partition of X ;

reconsider EEE = E as Relation of X,X ;

now :: thesis: for e, f1, f2 being object st [e,f1] in f quotient (E,F) & [e,f2] in f quotient (E,F) holds

f1 = f2

hence
for bf1 = f2

let e, f1, f2 be object ; :: thesis: ( [e,f1] in f quotient (E,F) & [e,f2] in f quotient (E,F) implies f1 = f2 )

assume [e,f1] in f quotient (E,F) ; :: thesis: ( [e,f2] in f quotient (E,F) implies f1 = f2 )

then consider ee1 being Element of Class E, ff1 being Element of Class F such that

A1: ( [e,f1] = [ee1,ff1] & ex x1, y1 being set st

( x1 in ee1 & y1 in ff1 & [x1,y1] in f ) ) ;

consider x1, y1 being set such that

A2: ( x1 in ee1 & y1 in ff1 & [x1,y1] in f ) by A1;

assume [e,f2] in f quotient (E,F) ; :: thesis: f1 = f2

then consider ee2 being Element of Class E, ff2 being Element of Class F such that

A3: ( [e,f2] = [ee2,ff2] & ex x2, y2 being set st

( x2 in ee2 & y2 in ff2 & [x2,y2] in f ) ) ;

A4: ( ee1 = e & ee2 = e & ff1 = f1 & ff2 = f2 ) by A1, A3, XTUPLE_0:1;

consider x2, y2 being set such that

A5: ( x2 in ee2 & y2 in ff2 & [x2,y2] in f ) by A3;

A6: [x1,x2] in E by Lm9, A2, A5, A4;

( y2 = f . x2 & y1 = f . x1 ) by A5, A2, FUNCT_1:1;

then [y1,y2] in F by Def9, A6;

hence f1 = f2 by A4, A2, A5, Lm10; :: thesis: verum

end;assume [e,f1] in f quotient (E,F) ; :: thesis: ( [e,f2] in f quotient (E,F) implies f1 = f2 )

then consider ee1 being Element of Class E, ff1 being Element of Class F such that

A1: ( [e,f1] = [ee1,ff1] & ex x1, y1 being set st

( x1 in ee1 & y1 in ff1 & [x1,y1] in f ) ) ;

consider x1, y1 being set such that

A2: ( x1 in ee1 & y1 in ff1 & [x1,y1] in f ) by A1;

assume [e,f2] in f quotient (E,F) ; :: thesis: f1 = f2

then consider ee2 being Element of Class E, ff2 being Element of Class F such that

A3: ( [e,f2] = [ee2,ff2] & ex x2, y2 being set st

( x2 in ee2 & y2 in ff2 & [x2,y2] in f ) ) ;

A4: ( ee1 = e & ee2 = e & ff1 = f1 & ff2 = f2 ) by A1, A3, XTUPLE_0:1;

consider x2, y2 being set such that

A5: ( x2 in ee2 & y2 in ff2 & [x2,y2] in f ) by A3;

A6: [x1,x2] in E by Lm9, A2, A5, A4;

( y2 = f . x2 & y1 = f . x1 ) by A5, A2, FUNCT_1:1;

then [y1,y2] in F by Def9, A6;

hence f1 = f2 by A4, A2, A5, Lm10; :: thesis: verum

b