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

proof

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

end;

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

proof

assume A4: b = 0. F ; :: thesis: (a * b) * c = a * (b * c)
hence (a * b) * c = (0. F) * c by VECTSP_1:6
.= 0. F by VECTSP_1:7
.= a * (0. F) by VECTSP_1:6
.= a * (b * c) by A4, VECTSP_1:7 ;
:: thesis: verum

end;

A5: ( 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:6
.= a * (0. F) by VECTSP_1:6
.= a * (b * c) by A6, VECTSP_1:6 ;
:: thesis: verum

end;

( 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 A1, A3, A5, Th8; :: thesis: verum