let V be non empty add-associative addLoopStr ; :: thesis: for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3)
let M1, M2, M3 be Subset of V; :: thesis: (M1 + M2) + M3 = M1 + (M2 + M3)
for x being Element of V st x in (M1 + M2) + M3 holds
x in M1 + (M2 + M3)

proof

let x be Element of V; :: thesis: ( x in (M1 + M2) + M3 implies x in M1 + (M2 + M3) )
assume x in (M1 + M2) + M3 ; :: thesis: x in M1 + (M2 + M3)
then consider x', x3 being Element of V such that
A1: ( x = x' + x3 & x' in M1 + M2 & x3 in M3 ) ;
consider x1, x2 being Element of V such that
A2: ( x' = x1 + x2 & x1 in M1 & x2 in M2 ) by A1;
A3: x = x1 + (x2 + x3) by A1, A2, RLVECT_1:def 6;
x2 + x3 in M2 + M3 by A1, A2;
hence x in M1 + (M2 + M3) by A2, A3; :: thesis: verum

end;

then A4: (M1 + M2) + M3 c= M1 + (M2 + M3) by SUBSET_1:7;
for x being Element of V st x in M1 + (M2 + M3) holds
x in (M1 + M2) + M3

proof

let x be Element of V; :: thesis: ( x in M1 + (M2 + M3) implies x in (M1 + M2) + M3 )
assume x in M1 + (M2 + M3) ; :: thesis: x in (M1 + M2) + M3
then consider x1, x' being Element of V such that
A5: ( x = x1 + x' & x1 in M1 & x' in M2 + M3 ) ;
consider x2, x3 being Element of V such that
A6: ( x' = x2 + x3 & x2 in M2 & x3 in M3 ) by A5;
A7: x = (x1 + x2) + x3 by A5, A6, RLVECT_1:def 6;
x1 + x2 in M1 + M2 by A5, A6;
hence x in (M1 + M2) + M3 by A6, A7; :: thesis: verum

end;

then M1 + (M2 + M3) c= (M1 + M2) + M3 by SUBSET_1:7;
hence (M1 + M2) + M3 = M1 + (M2 + M3) by A4, XBOOLE_0:def 10; :: thesis: verum