defpred S1[ Element of S, Element of S, Element of S] means w . ($1,$3) = w . ($3,$2);
A2:
for a, b being Element of S ex c being Element of S st S1[a,b,c]
proof
let a,
b be
Element of
S;
ex c being Element of S st S1[a,b,c]
set x =
Half (w . (a,b));
consider c being
Element of
S such that A3:
w . (
a,
c)
= Half (w . (a,b))
by A1;
take
c
;
S1[a,b,c]
(Half (w . (a,b))) + (Half (w . (a,b))) =
Double (Half (w . (a,b)))
.=
w . (
a,
b)
by Def6
.=
(Half (w . (a,b))) + (w . (c,b))
by A1, A3
;
hence
S1[
a,
b,
c]
by A3, RLVECT_1:8;
verum
end;
consider o being BinOp of S such that
A4:
for a, b being Element of S holds S1[a,b,o . (a,b)]
from BINOP_1:sch 3(A2);
take
o
; for a, b being Element of S holds w . (a,(o . (a,b))) = w . ((o . (a,b)),b)
thus
for a, b being Element of S holds w . (a,(o . (a,b))) = w . ((o . (a,b)),b)
by A4; verum