let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; :: thesis: for a being Element of NonZero F ex b being Element of NonZero F st
( a * b = 1. F & b * a = 1. F )
let a be Element of NonZero F; :: thesis: ex b being Element of NonZero F st
( a * b = 1. F & b * a = 1. F )
set B = H1(F) \ {(0. F)};
set P = (omf F) ! (H1(F),(0. F));
A1: H1(F) \ {(0. F)} = NonZero F ;
then reconsider e = 1. F as Element of H1(F) \ {(0. F)} by STRUCT_0:2;
addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! (H1(F),(0. F))),e #) is AbGroup by A1, Def4;
then consider D being strict AbGroup such that
A2: D = addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! (H1(F),(0. F))),e #) ;
reconsider a = a as Element of D by A2;
consider b being Element of D such that
A3: a + b = 0. D and
A4: b + a = 0. D by Th3;
reconsider b = b as Element of NonZero F by A2;
take b ; :: thesis: ( a * b = 1. F & b * a = 1. F )
(omf F) || (H1(F) \ {(0. F)}) is Function of [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):],(H1(F) \ {(0. F)}) by REALSET1:7;
then A5: dom ((omf F) || (H1(F) \ {(0. F)})) = [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] by FUNCT_2:def 1;
for x, y being Element of H1(F) \ {(0. F)} holds (omf F) . (x,y) = the addF of D . (x,y)
proof
let x, y be Element of H1(F) \ {(0. F)}; :: thesis: (omf F) . (x,y) = the addF of D . (x,y)
[x,y] in [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] ;
hence (omf F) . (x,y) = the addF of D . (x,y) by A2, A5, FUNCT_1:47; :: thesis: verum
end;
hence ( a * b = 1. F & b * a = 1. F ) by A2, A3, A4; :: thesis: verum