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

A4: for a, b being Element of S holds S_{1}[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

A2: for a, b being Element of S ex c being Element of S st S

proof

consider o being BinOp of S such that
let a, b be Element of S; :: thesis: ex c being Element of S st S_{1}[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_{1}[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_{1}[a,b,c]
by A3, RLVECT_1:8; :: thesis: verum

end;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

(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

A4: for a, b being Element of S holds S

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