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