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