defpred S₁[ Element of S, Element of S, Element of S] means w . $1,$3 = w . $3,$2;
A5: for a, b, c, c9 being Element of S st S₁[a,b,c] & S₁[a,b,c9] holds
c = c9

proof

let a, b, c, c9 be Element of S; :: thesis: ( S₁[a,b,c] & S₁[a,b,c9] implies c = c9 )
assume A6: ( S₁[a,b,c] & S₁[a,b,c9] ) ; :: thesis: c = c9
w . c,c9 = (w . c,a) + (w . a,c9) by A1, Def3
.= (w . c9,b) + (w . b,c) by A1, A6, Th7
.= w . c9,c by A1, Def3
.= - (w . c,c9) by A1, Th6 ;
then w . c,c9 = 0. G by Th19;
hence c = c9 by A1, Th5; :: thesis: verum

end;

let f, g be BinOp of S; :: thesis: ( ( for a, b being Element of S holds w . a,(f . a,b) = w . (f . a,b),b ) & ( for a, b being Element of S holds w . a,(g . a,b) = w . (g . a,b),b ) implies f = g )
assume A7: ( ( for a, b being Element of S holds w . a,(f . a,b) = w . (f . a,b),b ) & ( for a, b being Element of S holds w . a,(g . a,b) = w . (g . a,b),b ) ) ; :: thesis: f = g
for a, b being Element of S holds f . a,b = g . a,b

proof

let a, b be Element of S; :: thesis: f . a,b = g . a,b
( w . a,(f . a,b) = w . (f . a,b),b & w . a,(g . a,b) = w . (g . a,b),b ) by A7;
hence f . a,b = g . a,b by A5; :: thesis: verum

end;

hence f = g by BINOP_1:2; :: thesis: verum