let V be non empty add-associative addLoopStr ; :: thesis: for A being Subset of V

for v, w being Element of V holds (v + w) + A = v + (w + A)

let A be Subset of V; :: thesis: for v, w being Element of V holds (v + w) + A = v + (w + A)

let v, w be Element of V; :: thesis: (v + w) + A = v + (w + A)

set vw = v + w;

thus (v + w) + A c= v + (w + A) :: according to XBOOLE_0:def 10 :: thesis: v + (w + A) c= (v + w) + A

assume x in v + (w + A) ; :: thesis: x in (v + w) + A

then consider s being Element of V such that

A2: x = v + s and

A3: s in w + A ;

consider r being Element of V such that

A4: s = w + r and

A5: r in A by A3;

x = (v + w) + r by A2, A4, RLVECT_1:def 3;

hence x in (v + w) + A by A5; :: thesis: verum

for v, w being Element of V holds (v + w) + A = v + (w + A)

let A be Subset of V; :: thesis: for v, w being Element of V holds (v + w) + A = v + (w + A)

let v, w be Element of V; :: thesis: (v + w) + A = v + (w + A)

set vw = v + w;

thus (v + w) + A c= v + (w + A) :: according to XBOOLE_0:def 10 :: thesis: v + (w + A) c= (v + w) + A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v + (w + A) or x in (v + w) + A )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (v + w) + A or x in v + (w + A) )

assume x in (v + w) + A ; :: thesis: x in v + (w + A)

then consider s being Element of V such that

A1: ( x = (v + w) + s & s in A ) ;

( w + s in w + A & x = v + (w + s) ) by A1, RLVECT_1:def 3;

hence x in v + (w + A) ; :: thesis: verum

end;assume x in (v + w) + A ; :: thesis: x in v + (w + A)

then consider s being Element of V such that

A1: ( x = (v + w) + s & s in A ) ;

( w + s in w + A & x = v + (w + s) ) by A1, RLVECT_1:def 3;

hence x in v + (w + A) ; :: thesis: verum

assume x in v + (w + A) ; :: thesis: x in (v + w) + A

then consider s being Element of V such that

A2: x = v + s and

A3: s in w + A ;

consider r being Element of V such that

A4: s = w + r and

A5: r in A by A3;

x = (v + w) + r by A2, A4, RLVECT_1:def 3;

hence x in (v + w) + A by A5; :: thesis: verum