let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; :: thesis: for a, b, c being Element of F holds (a * b) * c = a * (b * c)
let a, b, c be Element of H₁(F); :: thesis: (a * b) * c = a * (b * c)
( a = 0. F or b = 0. F or c = 0. F or ( a is Element of NonZero F & b is Element of NonZero F & c is Element of NonZero F ) ) by ZFMISC_1:56;
hence (a * b) * c = a * (b * c) by Th4; :: thesis: verum