let E be non empty add-associative addLoopStr ; :: thesis: for A, B, C being Subset of E holds (A + B) + C = A + (B + C)

let A, B, C be Subset of E; :: thesis: (A + B) + C = A + (B + C)

for x being Element of E holds

( x in (A + B) + C iff x in A + (B + C) )

let A, B, C be Subset of E; :: thesis: (A + B) + C = A + (B + C)

for x being Element of E holds

( x in (A + B) + C iff x in A + (B + C) )

proof

hence
(A + B) + C = A + (B + C)
by SUBSET_1:3; :: thesis: verum
let x be Element of E; :: thesis: ( x in (A + B) + C iff x in A + (B + C) )

then consider a, bc being Element of E such that

A4: ( x = a + bc & a in A & bc in B + C ) ;

consider b, c being Element of E such that

A5: ( bc = b + c & b in B & c in C ) by A4;

A6: x = (a + b) + c by A4, A5, RLVECT_1:def 3;

a + b in A + B by A4, A5;

hence x in (A + B) + C by A5, A6; :: thesis: verum

end;hereby :: thesis: ( x in A + (B + C) implies x in (A + B) + C )

assume
x in A + (B + C)
; :: thesis: x in (A + B) + Cassume
x in (A + B) + C
; :: thesis: x in A + (B + C)

then consider ab, c being Element of E such that

A1: ( x = ab + c & ab in A + B & c in C ) ;

consider a, b being Element of E such that

A2: ( ab = a + b & a in A & b in B ) by A1;

A3: x = a + (b + c) by A1, A2, RLVECT_1:def 3;

b + c in B + C by A1, A2;

hence x in A + (B + C) by A2, A3; :: thesis: verum

end;then consider ab, c being Element of E such that

A1: ( x = ab + c & ab in A + B & c in C ) ;

consider a, b being Element of E such that

A2: ( ab = a + b & a in A & b in B ) by A1;

A3: x = a + (b + c) by A1, A2, RLVECT_1:def 3;

b + c in B + C by A1, A2;

hence x in A + (B + C) by A2, A3; :: thesis: verum

then consider a, bc being Element of E such that

A4: ( x = a + bc & a in A & bc in B + C ) ;

consider b, c being Element of E such that

A5: ( bc = b + c & b in B & c in C ) by A4;

A6: x = (a + b) + c by A4, A5, RLVECT_1:def 3;

a + b in A + B by A4, A5;

hence x in (A + B) + C by A5, A6; :: thesis: verum