defpred S_{1}[ 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_{1}[a,b,c] & S_{1}[a,b,c9] holds

c = c9

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)

A5: for a, b, c, c9 being Element of S st S

c = c9

proof

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 )
let a, b, c, c9 be Element of S; :: thesis: ( S_{1}[a,b,c] & S_{1}[a,b,c9] implies c = c9 )

assume A6: ( S_{1}[a,b,c] & S_{1}[a,b,c9] )
; :: thesis: c = c9

w . (c,c9) = (w . (c,a)) + (w . (a,c9)) by A1

.= (w . (c9,b)) + (w . (b,c)) by A1, A6, Th5

.= w . (c9,c) by A1

.= - (w . (c,c9)) by A1, Th4 ;

then w . (c,c9) = 0. G by Th16;

hence c = c9 by A1, Th3; :: thesis: verum

end;assume A6: ( S

w . (c,c9) = (w . (c,a)) + (w . (a,c9)) by A1

.= (w . (c9,b)) + (w . (b,c)) by A1, A6, Th5

.= w . (c9,c) by A1

.= - (w . (c,c9)) by A1, Th4 ;

then w . (c,c9) = 0. G by Th16;

hence c = c9 by A1, Th3; :: thesis: verum

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

hence
f = g
by BINOP_1:2; :: thesis: verum
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;( 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