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

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