let b1, b2 be BinOp of (Class R); ( ( 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)))
; b1 = b2
now for x, y being Element of Class R holds b1 . (x,y) = b2 . (x,y)let x,
y be
Element of
Class R;
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;
verum end;
hence
b1 = b2
; verum