defpred S_{1}[ Element of rng r, Element of rng r, Element of rng r] means $3 = r . (((r ") . $1) + ((r ") . $2));

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

A: now :: thesis: for x, y being Element of rng r ex z being Element of rng r st S_{1}[x,y,z]

consider F being BinOp of (rng r) such that let x, y be Element of rng r; :: thesis: ex z being Element of rng r st S_{1}[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_{1}[x,y,z]
; :: thesis: verum

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

B: for a, b being Element of rng r holds S

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