defpred S₁[ object , object ] means (omf F) . ($1,$2) = 1. F;
A1: for x being object st x in H₁(F) \ {(0. F)} holds
ex y being object st
( y in H₁(F) \ {(0. F)} & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in H₁(F) \ {(0. F)} implies ex y being object st
( y in H₁(F) \ {(0. F)} & S₁[x,y] ) )
assume x in H₁(F) \ {(0. F)} ; :: thesis: ex y being object st
( y in H₁(F) \ {(0. F)} & S₁[x,y] )
then reconsider x = x as Element of NonZero F ;
consider y being Element of H₁(F) \ {(0. F)} such that
A2: x * y = 1. F and
y * x = 1. F by Th7;
reconsider y = y as set ;
take y ; :: thesis: ( y in H₁(F) \ {(0. F)} & S₁[x,y] )
thus ( y in H₁(F) \ {(0. F)} & S₁[x,y] ) by A2; :: thesis: verum

end;

ex C being Function of (H₁(F) \ {(0. F)}),(H₁(F) \ {(0. F)}) st
for x being object st x in H₁(F) \ {(0. F)} holds
S₁[x,C . x] from FUNCT_2:sch 1(A1);
then consider C being UnOp of (NonZero F) such that
A3: for x being object st x in H₁(F) \ {(0. F)} holds
(omf F) . (x,(C . x)) = 1. F ;
take C ; :: thesis: for x being Element of NonZero F holds (omf F) . (x,(C . x)) = 1. F
thus for x being Element of NonZero F holds (omf F) . (x,(C . x)) = 1. F by A3; :: thesis: verum