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 object holds
( x in (v + A) (+) B iff x in A (+) (v + B) )

proof

let x be object ; :: 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
A1: ( x = f + b & f in v + A & b in B ) ;
consider a being Element of E such that
A2: ( f = v + a & a in A ) by A1;
A3: x = a + (v + b) by A1, A2, RLVECT_1:def 3;
v + b in v + B by A1;
hence x in A (+) (v + B) by A3, A2; :: 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
A4: ( x = a + f & a in A & f in v + B ) ;
consider b being Element of E such that
A5: ( f = v + b & b in B ) by A4;
A6: x = (v + a) + b by A4, A5, RLVECT_1:def 3;
v + a in v + A by A4;
hence x in (v + A) (+) B by A6, A5; :: thesis: verum

end;

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

proof

let x be object ; :: 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
A7: ( x = f + b & f in v + A & b in B ) ;
consider a being Element of E such that
A8: ( f = v + a & a in A ) by A7;
A9: x = v + (a + b) by A7, A8, RLVECT_1:def 3;
a + b in A + B by A7, A8;
hence x in v + (A (+) B) by A9; :: thesis: verum

end;

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

end;

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