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
x in { (u + v) where u, v is Element of V : ( u in M1 + M2 & v in M3 ) }
by RUSUB_4:def 10;
then consider x',
x3 being
Element of
V such that A1:
(
x = x' + x3 &
x' in M1 + M2 &
x3 in M3 )
;
x' in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 ) }
by A1, RUSUB_4:def 10;
then consider x1,
x2 being
Element of
V such that A2:
(
x' = x1 + x2 &
x1 in M1 &
x2 in M2 )
;
A3:
x = x1 + (x2 + x3)
by A1, A2, RLVECT_1:def 6;
x2 + x3 in { (u + v) where u, v is Element of V : ( u in M2 & v in M3 ) }
by A1, A2;
then
x2 + x3 in M2 + M3
by RUSUB_4:def 10;
then
x in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 + M3 ) }
by A2, A3;
hence
x in M1 + (M2 + M3)
by RUSUB_4:def 10;
:: 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
x in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 + M3 ) }
by RUSUB_4:def 10;
then consider x1,
x' being
Element of
V such that A5:
(
x = x1 + x' &
x1 in M1 &
x' in M2 + M3 )
;
x' in { (u + v) where u, v is Element of V : ( u in M2 & v in M3 ) }
by A5, RUSUB_4:def 10;
then consider x2,
x3 being
Element of
V such that A6:
(
x' = x2 + x3 &
x2 in M2 &
x3 in M3 )
;
A7:
x = (x1 + x2) + x3
by A5, A6, RLVECT_1:def 6;
x1 + x2 in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 ) }
by A5, A6;
then
x1 + x2 in M1 + M2
by RUSUB_4:def 10;
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 10;
:: 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