let b1, b2 be BinOp of (); :: thesis: ( ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b1 . (x,y) = Class (R,(b . (x1,y1))) ) & ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b2 . (x,y) = Class (R,(b . (x1,y1))) ) implies b1 = b2 )

assume that
A18: for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b1 . (x,y) = Class (R,(b . (x1,y1))) and
A19: for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b2 . (x,y) = Class (R,(b . (x1,y1))) ; :: thesis: b1 = b2
now :: thesis: for x, y being Element of Class R holds b1 . (x,y) = b2 . (x,y)
let x, y be Element of Class R; :: thesis: b1 . (x,y) = b2 . (x,y)
consider x1 being object such that
A20: x1 in D and
A21: x = Class (R,x1) by EQREL_1:def 3;
consider y1 being object such that
A22: y1 in D and
A23: y = Class (R,y1) by EQREL_1:def 3;
A24: y1 in y by ;
A25: x1 in x by ;
then b1 . (x,y) = Class (R,(b . (x1,y1))) by ;
hence b1 . (x,y) = b2 . (x,y) by ; :: thesis: verum
end;
hence b1 = b2 ; :: thesis: verum