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)
A1: ( a = 0. F or b = 0. F or c = 0. F or ( a is Element of H₁(F) \ {(0. F)} & b is Element of H₁(F) \ {(0. F)} & c is Element of H₁(F) \ {(0. F)} ) ) by ZFMISC_1:64;
A2: ( a = 0. F implies (a * b) * c = a * (b * c) )

proof

assume A3: a = 0. F ; :: thesis: (a * b) * c = a * (b * c)
hence (a * b) * c = (0. F) * c by VECTSP_1:39
.= 0. F by VECTSP_1:39
.= a * (b * c) by A3, VECTSP_1:39 ;
:: thesis: verum

end;

A4: ( b = 0. F implies (a * b) * c = a * (b * c) )

proof

assume A5: b = 0. F ; :: thesis: (a * b) * c = a * (b * c)
hence (a * b) * c = (0. F) * c by VECTSP_1:36
.= 0. F by VECTSP_1:39
.= a * (0. F) by VECTSP_1:36
.= a * (b * c) by A5, VECTSP_1:39 ;
:: thesis: verum

end;

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

proof

assume A6: c = 0. F ; :: thesis: (a * b) * c = a * (b * c)
hence (a * b) * c = 0. F by VECTSP_1:36
.= a * (0. F) by VECTSP_1:36
.= a * (b * c) by A6, VECTSP_1:36 ;
:: thesis: verum

end;

hence (a * b) * c = a * (b * c) by A1, A2, A4, Th8; :: thesis: verum