defpred S₁[ Element of rng r, Element of rng r, Element of rng r] means $3 = r . (((r ") . $1) * ((r ") . $2));

A: now :: thesis: for x, y being Element of rng r ex z being Element of rng r st S₁[x,y,z]

let x, y be Element of rng r; :: thesis: ex z being Element of rng r st S₁[x,y,z]
set z = r . (((r ") . x) * ((r ") . y));
dom r = the carrier of F by defr;
then r . (((r ") . x) * ((r ") . y)) in rng r by FUNCT_1:3;
hence ex z being Element of rng r st S₁[x,y,z] ; :: thesis: verum

end;

consider F being BinOp of (rng r) such that
B: for a, b being Element of rng r holds S₁[a,b,F . (a,b)] from BINOP_1:sch 3(A);
take F ; :: thesis: 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; :: thesis: F . (a,b) = r . (((r ") . a) * ((r ") . b))
thus F . (a,b) = r . (((r ") . a) * ((r ") . b)) by B; :: thesis: verum