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 implies a * b = b * a )

proof

assume A2: a = 0. F ; :: thesis: a * b = b * a
then a * b = 0. F by VECTSP_1:7
.= b * a by A2, VECTSP_1:6 ;
hence a * b = b * a ; :: thesis: verum

end;

A3: ( 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:6
.= b * a by A4, VECTSP_1:7 ;
hence a * b = b * a ; :: thesis: verum

end;

( a = 0. F or b = 0. F or ( a is Element of NonZero F & b is Element of NonZero F ) ) by ZFMISC_1:56;
hence a * b = b * a by A1, A3, Th9; :: thesis: verum