let o1, o2 be BinOp of Class E; :: thesis: ( ( 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 A4:
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)
; :: thesis: ( 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 A5:
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)
; :: thesis: o1 = o2
now let W1,
W2 be
Element of
Class E;
:: thesis: o1 . W1,W2 = o2 . W1,W2consider x being
set such that A6:
(
x in the
carrier of
X &
W1 = Class E,
x )
by EQREL_1:def 5;
consider y being
set such that A7:
(
y in the
carrier of
X &
W2 = Class E,
y )
by EQREL_1:def 5;
reconsider x =
x,
y =
y as
Element of
X by A6, A7;
o1 . W1,
W2 = Class E,
(x \ y)
by A4, A6, A7;
hence
o1 . W1,
W2 = o2 . W1,
W2
by A5, A6, A7;
:: thesis: verum end;
hence
o1 = o2
by BINOP_1:2; :: thesis: verum