let F be Field; :: thesis: for a, b, c, d being Element of F holds (c * d) * (a * b) = ((a * c) * d) * b
let a, b, c, d 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 3
.= ((a * c) * d) * b by GROUP_1:def 3 ; :: thesis: verum