let E be RealLinearSpace; :: thesis: for A, B being Subset of E st B = the carrier of E & A <> {} holds
( A (+) B = B & B (+) A = B )
let A, B be Subset of E; :: thesis: ( B = the carrier of E & A <> {} implies ( A (+) B = B & B (+) A = B ) )
assume A1: ( B = the carrier of E & A <> {} ) ; :: thesis: ( A (+) B = B & B (+) A = B )
then consider a being object such that
A2: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of E by A2;
now :: thesis: for x being object st x in the carrier of E holds
x in A (+) B
let x be object ; :: thesis: ( x in the carrier of E implies x in A (+) B )
assume x in the carrier of E ; :: thesis: x in A (+) B
then reconsider z = x as Element of E ;
a + (z - a) = z by RLVECT_4:1;
hence x in A (+) B by A1, A2; :: thesis: verum
end;
then A3: the carrier of E c= A (+) B ;
hence B = A (+) B by A1; :: thesis: B (+) A = B
thus B (+) A = A + B
.= B by A3, A1 ; :: thesis: verum