let F be Field; :: thesis: for c, d, a, b being Element of F holds (c * d) * (a * b) = ((a * c) * d) * b
let c, d, a, b be Element of F; :: thesis: (c * d) * (a * b) = ((a * c) * d) * b
thus (c * d) * (a * b) = (a * (c * d)) * b by GROUP_1:def 4
.= ((a * c) * d) * b by GROUP_1:def 4 ; :: thesis: verum