defpred S1[ Element of rng r, Element of rng r, Element of rng r] means $3 = r . (((r ") . $1) * ((r ") . $2));
consider F being BinOp of (rng r) such that
B:
for a, b being Element of rng r holds S1[a,b,F . (a,b)]
from BINOP_1:sch 3(A);
take
F
; for a, b being Element of rng r holds F . (a,b) = r . (((r ") . a) * ((r ") . b))
let a, b be Element of rng r; F . (a,b) = r . (((r ") . a) * ((r ") . b))
thus
F . (a,b) = r . (((r ") . a) * ((r ") . b))
by B; verum