let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; for a, b being Element of NonZero F holds a * b = b * a
let a, b be Element of NonZero F; a * b = b * a
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;
reconsider D = addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! (H1(F),(0. F))),e #) as strict AbGroup by A1, Def4;
reconsider a = a, b = b as Element of D ;
reconsider x = a, y = b as Element of 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 A2:
dom ((omf F) || (H1(F) \ {(0. F)})) = [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):]
by FUNCT_2:def 1;
A3:
for x, y being Element of H1(F) \ {(0. F)} holds (omf F) . (x,y) = the addF of D . (x,y)
then x * y =
a + b
.=
b + a
.=
y * x
by A3
;
hence
a * b = b * a
; verum