let b1, b2 be BinOp of (Class R); :: 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

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)

hence
b1 = b2
; :: thesis: verumlet 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 A22, A23, EQREL_1:20;

A25: x1 in x by A20, A21, EQREL_1:20;

then b1 . (x,y) = Class (R,(b . (x1,y1))) by A18, A24;

hence b1 . (x,y) = b2 . (x,y) by A19, A25, A24; :: thesis: verum

end;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 A22, A23, EQREL_1:20;

A25: x1 in x by A20, A21, EQREL_1:20;

then b1 . (x,y) = Class (R,(b . (x1,y1))) by A18, A24;

hence b1 . (x,y) = b2 . (x,y) by A19, A25, A24; :: thesis: verum