defpred S₁[ Element of F, Element of NonZero F, set ] means $3 = (omf F) . $1,((revf F) . $2);

now

let x be Element of F; :: thesis: for y being Element of NonZero F ex z being Element of F st z = (omf F) . x,((revf F) . y)
let y be Element of NonZero F; :: thesis: ex z being Element of F st z = (omf F) . x,((revf F) . y)
(revf F) . y is Element of F by XBOOLE_0:def 5;
then reconsider z = (omf F) . x,((revf F) . y) as Element of F by REALSET2:14;
take z = z; :: thesis: z = (omf F) . x,((revf F) . y)
thus z = (omf F) . x,((revf F) . y) ; :: thesis: verum

end;

then A1: for x being Element of F
for y being Element of NonZero F ex z being Element of F st S₁[x,y,z] ;
ex f being Function of [:the carrier of F,(NonZero F):],the carrier of F st
for x being Element of F
for y being Element of NonZero F holds S₁[x,y,f . x,y] from BINOP_1:sch 3(A1);
hence ex b₁ being Function of [:the carrier of F,(NonZero F):],the carrier of F st
for x being Element of F
for y being Element of NonZero F holds b₁ . x,y = (omf F) . x,((revf F) . y) ; :: thesis: verum