let R be non empty add-associative addLoopStr ; :: thesis: for I, J, K being Subset of R holds I + (J + K) = (I + J) + K
let I, J, K be Subset of R; :: thesis: I + (J + K) = (I + J) + K

A1: now :: thesis: for u being object st u in (I + J) + K holds
u in I + (J + K)

let u be object ; :: thesis: ( u in (I + J) + K implies u in I + (J + K) )
assume u in (I + J) + K ; :: thesis: u in I + (J + K)
then consider a, b being Element of R such that
A2: u = a + b and
A3: a in I + J and
A4: b in K ;
consider c, d being Element of R such that
A5: a = c + d and
A6: c in I and
A7: d in J by A3;
d + b in { (a9 + b9) where a9, b9 is Element of R : ( a9 in J & b9 in K ) } by A4, A7;
then c + (d + b) in { (a9 + b9) where a9, b9 is Element of R : ( a9 in I & b9 in J + K ) } by A6;
hence u in I + (J + K) by A2, A5, RLVECT_1:def 3; :: thesis: verum

end;

now :: thesis: for u being object st u in I + (J + K) holds
u in (I + J) + K

let u be object ; :: thesis: ( u in I + (J + K) implies u in (I + J) + K )
assume u in I + (J + K) ; :: thesis: u in (I + J) + K
then consider a, b being Element of R such that
A8: u = a + b and
A9: a in I and
A10: b in J + K ;
consider c, d being Element of R such that
A11: b = c + d and
A12: c in J and
A13: d in K by A10;
a + c in { (a9 + b9) where a9, b9 is Element of R : ( a9 in I & b9 in J ) } by A9, A12;
then (a + c) + d in { (a9 + b9) where a9, b9 is Element of R : ( a9 in I + J & b9 in K ) } by A13;
hence u in (I + J) + K by A8, A11, RLVECT_1:def 3; :: thesis: verum

end;

hence I + (J + K) = (I + J) + K by A1, TARSKI:2; :: thesis: verum