let F be Field; :: thesis: the multF of F is associative
let x, y, z be Element of F; :: according to BINOP_1:def 14 :: thesis: the multF of F . x,(the multF of F . y,z) = the multF of F . (the multF of F . x,y),z
thus the multF of F . x,(the multF of F . y,z) = x * (y * z)
.= (x * y) * z by GROUP_1:def 4
.= the multF of F . (the multF of F . x,y),z ; :: thesis: verum