let K be Field; :: thesis: 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; :: thesis: 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 ; :: thesis: verum