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
( 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 Th5; :: thesis: verum