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 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) ; :: 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 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) ; :: thesis: o1 = o2

now

let W1, W2 be Element of Class E; :: thesis: o1 . W1,W2 = o2 . W1,W2
consider x being set such that
A11: x in the carrier of X and
A12: W1 = Class E,x by EQREL_1:def 5;
consider y being set such that
A13: y in the carrier of X and
A14: W2 = Class E,y by EQREL_1:def 5;
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; :: thesis: verum

end;

hence o1 = o2 by BINOP_1:2; :: thesis: verum