let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; :: thesis: for a being Element of the carrier of F \ {(0. F)} ex b being Element of the carrier of F \ {(0. F)} st
( a * b = 1. F & b * a = 1. F )
let a be Element of H₁(F) \ {(0. F)}; :: thesis: ex b being Element of the carrier of F \ {(0. F)} st
( a * b = 1. F & b * a = 1. F )
set B = H₁(F) \ {(0. F)};
set P = (omf F) ! H₁(F),(0. F);
reconsider e = 1. F as Element of H₁(F) \ {(0. F)} by Lm26;
addLoopStr(# (H₁(F) \ {(0. F)}),((omf F) ! H₁(F),(0. F)),e #) is AbGroup by Def11;
then consider D being strict AbGroup such that
A1: D = addLoopStr(# (H₁(F) \ {(0. F)}),((omf F) ! H₁(F),(0. F)),e #) ;
reconsider a = a as Element of D by A1;
consider b being Element of D such that
A2: ( a + b = 0. D & b + a = 0. D ) by Th7;
(omf F) || (H₁(F) \ {(0. F)}) is Function of [:(H₁(F) \ {(0. F)}),(H₁(F) \ {(0. F)}):],H₁(F) \ {(0. F)} by REALSET1:11;
then A3: dom ((omf F) || (H₁(F) \ {(0. F)})) = [:(H₁(F) \ {(0. F)}),(H₁(F) \ {(0. F)}):] by FUNCT_2:def 1;
A4: for x, y being Element of H₁(F) \ {(0. F)} holds (omf F) . x,y = the addF of D . x,y

proof

let x, y be Element of H₁(F) \ {(0. F)}; :: thesis: (omf F) . x,y = the addF of D . x,y
[x,y] in [:(H₁(F) \ {(0. F)}),(H₁(F) \ {(0. F)}):] ;
hence (omf F) . x,y = the addF of D . x,y by A1, A3, FUNCT_1:70; :: thesis: verum

end;

reconsider b = b as Element of H₁(F) \ {(0. F)} by A1;
take b ; :: thesis: ( a * b = 1. F & b * a = 1. F )
thus ( a * b = 1. F & b * a = 1. F ) by A1, A2, A4; :: thesis: verum