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;

hence B = A (+) B by A1; :: thesis: B (+) A = B

thus B (+) A = A + B

.= B by A3, A1 ; :: thesis: verum

( 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

then A3:
the carrier of E c= A (+) B
;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;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

hence B = A (+) B by A1; :: thesis: B (+) A = B

thus B (+) A = A + B

.= B by A3, A1 ; :: thesis: verum