defpred S₁[ 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 S₁[a,b,c]

proof

let a, b be Element of S; :: thesis: ex c being Element of S st S₁[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 ; :: thesis: S₁[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 S₁[a,b,c] by A3, RLVECT_1:8; :: thesis: verum

end;

consider o being BinOp of S such that
A4: for a, b being Element of S holds S₁[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 A4; :: thesis: verum