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;
:: thesis: 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, Def3;
A4:
(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, Def3
;
take
c
;
:: thesis: S1[a,b,c]
thus
S1[
a,
b,
c]
by A3, A4, RLVECT_1:21;
:: thesis: verum
end;
consider o being BinOp of S such that
A5:
for a, b being Element of S holds S1[a,b,o . a,b]
from BINOP_1:sch 3(A2);
take
o
; :: thesis: 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 A5; :: thesis: verum