let K be Field; for a, b, c being Element of K holds the multF of K $$ <*a,b,c*> = (a * b) * c
let a, b, c be Element of K; the multF of K $$ <*a,b,c*> = (a * b) * c
the multF of K $$ <*a,b,c*> =
Product <*a,b,c*>
by GROUP_4:def 2
.=
(a * b) * c
by FVSUM_1:79
;
hence
the multF of K $$ <*a,b,c*> = (a * b) * c
; verum