let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; :: thesis: for a being Element of NonZero F holds
( a * (1. F) = a & (1. F) * a = a )
let a be Element of NonZero F; :: thesis: ( a * (1. F) = a & (1. F) * a = a )
set B = H₁(F) \ {(0. F)};
set P = (omf F) ! (H₁(F),(0. F));
A1: H₁(F) \ {(0. F)} = NonZero F ;
then reconsider e = 1. F as Element of H₁(F) \ {(0. F)} by STRUCT_0:2;
reconsider D = addLoopStr(# (H₁(F) \ {(0. F)}),((omf F) ! (H₁(F),(0. F))),e #) as strict AbGroup by A1, Def4;
reconsider a = a as Element of D ;
(omf F) || (H₁(F) \ {(0. F)}) is Function of [:(H₁(F) \ {(0. F)}),(H₁(F) \ {(0. F)}):],(H₁(F) \ {(0. F)}) by REALSET1:7;
then A2: dom ((omf F) || (H₁(F) \ {(0. F)})) = [:(H₁(F) \ {(0. F)}),(H₁(F) \ {(0. F)}):] by FUNCT_2:def 1;
A3: 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 A2, FUNCT_1:47; :: thesis: verum

end;

then A4: (omf F) . ((1. F),a) = (0. D) + a
.= a ;
(omf F) . (a,(1. F)) = a + (0. D) by A3
.= a ;
hence ( a * (1. F) = a & (1. F) * a = a ) by A4; :: thesis: verum