set IT = f quotient (E,F);
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

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;

hence for b₁ being Relation st b₁ = f quotient (E,F) holds
b₁ is Function-like by FUNCT_1:def 1; :: thesis: verum