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