let K be comRing; :: thesis: for a1, a2, a3, a4 being Element of K holds
( ((a1 * a2) * a3) * a4 = ((a4 * a2) * a3) * a1 & ((a1 * a2) * a3) * a4 = ((a1 * a4) * a3) * a2 )
let a1, a2, a3, a4 be Element of K; :: thesis: ( ((a1 * a2) * a3) * a4 = ((a4 * a2) * a3) * a1 & ((a1 * a2) * a3) * a4 = ((a1 * a4) * a3) * a2 )
thus ((a1 * a2) * a3) * a4 = ((a2 * a3) * a1) * a4 by GROUP_1:def 3
.= (a4 * (a2 * a3)) * a1 by GROUP_1:def 3
.= ((a4 * a2) * a3) * a1 by GROUP_1:def 3 ; :: thesis: ((a1 * a2) * a3) * a4 = ((a1 * a4) * a3) * a2
thus ((a1 * a2) * a3) * a4 = ((a1 * a3) * a2) * a4 by GROUP_1:def 3
.= ((a1 * a3) * a4) * a2 by GROUP_1:def 3
.= ((a1 * a4) * a3) * a2 by GROUP_1:def 3 ; :: thesis: verum