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