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

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