defpred S1[ 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 S1[a,b,c] & S1[a,b,c9] holds
c = c9
proof
let a, b, c, c9 be Element of S; :: thesis: ( S1[a,b,c] & S1[a,b,c9] implies c = c9 )
assume A6: ( S1[a,b,c] & S1[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;
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