let K be Abelian AddGroup; :: 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)
let a1, a2, a3, a4, a5, a6 be Element of K; :: 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 ALGSTR_1:7
.= a1 + (((a2 + a3) + a4) + (a5 + a6)) by Th8
.= a1 + ((((a2 + a3) + a4) + a5) + a6) by ALGSTR_1:7 ; :: thesis: verum