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

for y being Element of NonZero F ex z being Element of F st S_{1}[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_{1}[x,y,f . (x,y)]
from BINOP_1:sch 3(A1);

hence ex b_{1} 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_{1} . (x,y) = (omf F) . (x,((revf F) . y))
; :: thesis: verum

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))

then A1:
for x being Element of Ffor 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;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

for y being Element of NonZero F ex z being Element of F st S

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

hence ex b

for x being Element of F

for y being Element of NonZero F holds b