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

now :: thesis: for x being Element of F
for y being Element of NonZero F ex z being Element of F st z = (omf F) . (x,((revf F) . y))

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:10;
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