defpred S1[ 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 S1[x,y,z] ;
ex f being Function of [: the carrier of F,():], the carrier of F st
for x being Element of F
for y being Element of NonZero F holds S1[x,y,f . (x,y)] from hence ex b1 being Function of [: the carrier of F,():], the carrier of F st
for x being Element of F
for y being Element of NonZero F holds b1 . (x,y) = (omf F) . (x,((revf F) . y)) ; :: thesis: verum