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

for x being Element of V st x in (M1 + M2) + M3 holds

x in M1 + (M2 + M3)

hence (M1 + M2) + M3 = M1 + (M2 + M3) by A8; :: thesis: verum

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

then A8:
M1 + (M2 + M3) c= (M1 + M2) + M3
;
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 x in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 + M3 ) } by RUSUB_4:def 9;

then consider x1, x9 being Element of V such that

A1: x = x1 + x9 and

A2: x1 in M1 and

A3: x9 in M2 + M3 ;

x9 in { (u + v) where u, v is Element of V : ( u in M2 & v in M3 ) } by A3, RUSUB_4:def 9;

then consider x2, x3 being Element of V such that

A4: x9 = x2 + x3 and

A5: x2 in M2 and

A6: x3 in M3 ;

x1 + x2 in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 ) } by A2, A5;

then A7: x1 + x2 in M1 + M2 by RUSUB_4:def 9;

x = (x1 + x2) + x3 by A1, A4, RLVECT_1:def 3;

then x in { (u + v) where u, v is Element of V : ( u in M1 + M2 & v in M3 ) } by A6, A7;

hence x in (M1 + M2) + M3 by RUSUB_4:def 9; :: thesis: verum

end;assume x in M1 + (M2 + M3) ; :: thesis: x in (M1 + M2) + M3

then x in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 + M3 ) } by RUSUB_4:def 9;

then consider x1, x9 being Element of V such that

A1: x = x1 + x9 and

A2: x1 in M1 and

A3: x9 in M2 + M3 ;

x9 in { (u + v) where u, v is Element of V : ( u in M2 & v in M3 ) } by A3, RUSUB_4:def 9;

then consider x2, x3 being Element of V such that

A4: x9 = x2 + x3 and

A5: x2 in M2 and

A6: x3 in M3 ;

x1 + x2 in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 ) } by A2, A5;

then A7: x1 + x2 in M1 + M2 by RUSUB_4:def 9;

x = (x1 + x2) + x3 by A1, A4, RLVECT_1:def 3;

then x in { (u + v) where u, v is Element of V : ( u in M1 + M2 & v in M3 ) } by A6, A7;

hence x in (M1 + M2) + M3 by RUSUB_4:def 9; :: thesis: verum

for x being Element of V st x in (M1 + M2) + M3 holds

x in M1 + (M2 + M3)

proof

then
(M1 + M2) + M3 c= M1 + (M2 + M3)
;
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 x in { (u + v) where u, v is Element of V : ( u in M1 + M2 & v in M3 ) } by RUSUB_4:def 9;

then consider x9, x3 being Element of V such that

A9: x = x9 + x3 and

A10: x9 in M1 + M2 and

A11: x3 in M3 ;

x9 in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 ) } by A10, RUSUB_4:def 9;

then consider x1, x2 being Element of V such that

A12: x9 = x1 + x2 and

A13: x1 in M1 and

A14: x2 in M2 ;

x2 + x3 in { (u + v) where u, v is Element of V : ( u in M2 & v in M3 ) } by A11, A14;

then A15: x2 + x3 in M2 + M3 by RUSUB_4:def 9;

x = x1 + (x2 + x3) by A9, A12, RLVECT_1:def 3;

then x in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 + M3 ) } by A13, A15;

hence x in M1 + (M2 + M3) by RUSUB_4:def 9; :: thesis: verum

end;assume x in (M1 + M2) + M3 ; :: thesis: x in M1 + (M2 + M3)

then x in { (u + v) where u, v is Element of V : ( u in M1 + M2 & v in M3 ) } by RUSUB_4:def 9;

then consider x9, x3 being Element of V such that

A9: x = x9 + x3 and

A10: x9 in M1 + M2 and

A11: x3 in M3 ;

x9 in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 ) } by A10, RUSUB_4:def 9;

then consider x1, x2 being Element of V such that

A12: x9 = x1 + x2 and

A13: x1 in M1 and

A14: x2 in M2 ;

x2 + x3 in { (u + v) where u, v is Element of V : ( u in M2 & v in M3 ) } by A11, A14;

then A15: x2 + x3 in M2 + M3 by RUSUB_4:def 9;

x = x1 + (x2 + x3) by A9, A12, RLVECT_1:def 3;

then x in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 + M3 ) } by A13, A15;

hence x in M1 + (M2 + M3) by RUSUB_4:def 9; :: thesis: verum

hence (M1 + M2) + M3 = M1 + (M2 + M3) by A8; :: thesis: verum