let o1, o2 be BinOp of (Class E); ( ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
o1 . (W1,W2) = Class (E,(x \ y)) ) & ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
o2 . (W1,W2) = Class (E,(x \ y)) ) implies o1 = o2 )
assume A9:
for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
o1 . (W1,W2) = Class (E,(x \ y))
; ( ex W1, W2 being Element of Class E ex x, y being Element of X st
( W1 = Class (E,x) & W2 = Class (E,y) & not o2 . (W1,W2) = Class (E,(x \ y)) ) or o1 = o2 )
assume A10:
for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
o2 . (W1,W2) = Class (E,(x \ y))
; o1 = o2
now for W1, W2 being Element of Class E holds o1 . (W1,W2) = o2 . (W1,W2)let W1,
W2 be
Element of
Class E;
o1 . (W1,W2) = o2 . (W1,W2)consider x being
object such that A11:
x in the
carrier of
X
and A12:
W1 = Class (
E,
x)
by EQREL_1:def 3;
consider y being
object such that A13:
y in the
carrier of
X
and A14:
W2 = Class (
E,
y)
by EQREL_1:def 3;
reconsider x =
x,
y =
y as
Element of
X by A11, A13;
o1 . (
W1,
W2)
= Class (
E,
(x \ y))
by A9, A12, A14;
hence
o1 . (
W1,
W2)
= o2 . (
W1,
W2)
by A10, A12, A14;
verum end;
hence
o1 = o2
by BINOP_1:2; verum