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

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