let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; :: thesis: for a, b being Element of F holds a * b = b * a
let a, b be Element of H₁(F); :: thesis: a * b = b * a
A1: ( a = 0. F or b = 0. F or ( a is Element of H₁(F) \ {(0. F)} & b is Element of H₁(F) \ {(0. F)} ) ) by ZFMISC_1:64;
A2: ( a = 0. F implies a * b = b * a )

proof

assume A3: a = 0. F ; :: thesis: a * b = b * a
then a * b = 0. F by VECTSP_1:39
.= b * a by A3, VECTSP_1:36 ;
hence a * b = b * a ; :: thesis: verum

end;

( b = 0. F implies a * b = b * a )

proof

assume A4: b = 0. F ; :: thesis: a * b = b * a
then a * b = 0. F by VECTSP_1:36
.= b * a by A4, VECTSP_1:39 ;
hence a * b = b * a ; :: thesis: verum

end;

hence a * b = b * a by A1, A2, Th9; :: thesis: verum