let E be RealLinearSpace; :: thesis: for A, B being Subset of E st B = {} holds

( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )

let A, B be Subset of E; :: thesis: ( B = {} implies ( A (+) B = B & B (+) A = B & A (-) B = the carrier of E ) )

assume A1: B = {} ; :: thesis: ( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )

hence ( A (+) B = B & B (+) A = B ) by RUSUB_5:5; :: thesis: A (-) B = the carrier of E

hence the carrier of E = A (-) B ; :: thesis: verum

( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )

let A, B be Subset of E; :: thesis: ( B = {} implies ( A (+) B = B & B (+) A = B & A (-) B = the carrier of E ) )

assume A1: B = {} ; :: thesis: ( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )

hence ( A (+) B = B & B (+) A = B ) by RUSUB_5:5; :: thesis: A (-) B = the carrier of E

now :: thesis: for x being object st x in the carrier of E holds

x in A (-) B

then
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 ;

for b being Element of E st b in B holds

z - b in A by A1;

hence x in A (-) B ; :: thesis: verum

end;assume x in the carrier of E ; :: thesis: x in A (-) B

then reconsider z = x as Element of E ;

for b being Element of E st b in B holds

z - b in A by A1;

hence x in A (-) B ; :: thesis: verum

hence the carrier of E = A (-) B ; :: thesis: verum