let E be RealLinearSpace; :: thesis: for v being Element of E
for A, B being non empty binary-image of E holds
( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )
let v be Element of E; :: thesis: for A, B being non empty binary-image of E holds
( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )
let A, B be non empty binary-image of E; :: thesis: ( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )
for x being set holds
( x in (v + A) (+) B iff x in A (+) (v + B) )

proof

let x be set ; :: thesis: ( x in (v + A) (+) B iff x in A (+) (v + B) )

hereby :: thesis: ( x in A (+) (v + B) implies x in (v + A) (+) B )

assume x in (v + A) (+) B ; :: thesis: x in A (+) (v + B)
then consider f, b being Element of E such that
P1: ( x = f + b & f in v + A & b in B ) ;
consider a being Element of E such that
P2: ( f = v + a & a in A ) by P1;
P3: x = a + (v + b) by P1, P2, RLVECT_1:def 3;
v + b in v + B by P1;
hence x in A (+) (v + B) by P3, P2; :: thesis: verum

end;

assume x in A (+) (v + B) ; :: thesis: x in (v + A) (+) B
then consider a, f being Element of E such that
P1: ( x = a + f & a in A & f in v + B ) ;
consider b being Element of E such that
P2: ( f = v + b & b in B ) by P1;
P3: x = (v + a) + b by P1, P2, RLVECT_1:def 3;
v + a in v + A by P1;
hence x in (v + A) (+) B by P3, P2; :: thesis: verum

end;

hence (v + A) (+) B = A (+) (v + B) by TARSKI:1; :: thesis: (v + A) (+) B = v + (A (+) B)
for x being set holds
( x in (v + A) (+) B iff x in v + (A (+) B) )

proof

let x be set ; :: thesis: ( x in (v + A) (+) B iff x in v + (A (+) B) )

hereby :: thesis: ( x in v + (A (+) B) implies x in (v + A) (+) B )

assume x in (v + A) (+) B ; :: thesis: x in v + (A (+) B)
then consider f, b being Element of E such that
P1: ( x = f + b & f in v + A & b in B ) ;
consider a being Element of E such that
P2: ( f = v + a & a in A ) by P1;
P3: x = v + (a + b) by P1, P2, RLVECT_1:def 3;
a + b in A + B by P1, P2;
hence x in v + (A (+) B) by P3; :: thesis: verum

end;

assume x in v + (A (+) B) ; :: thesis: x in (v + A) (+) B
then consider ab being Element of E such that
P1: ( x = v + ab & ab in A (+) B ) ;
consider a, b being Element of E such that
P2: ( ab = a + b & a in A & b in B ) by P1;
P3: x = (v + a) + b by P1, P2, RLVECT_1:def 3;
v + a in v + A by P2;
hence x in (v + A) (+) B by P3, P2; :: thesis: verum

end;

hence (v + A) (+) B = v + (A (+) B) by TARSKI:1; :: thesis: verum