let F be Field; :: thesis: the multF of F is associative
let x, y, z be Element of F; :: according to BINOP_1:def 3 :: 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 3
.= the multF of F . (( the multF of F . (x,y)),z) ; :: thesis: verum