let V be RealLinearSpace; :: thesis: for W being strict Subspace of V holds
( ((0). V) + W = W & W + ((0). V) = W )
let W be strict Subspace of V; :: thesis: ( ((0). V) + W = W & W + ((0). V) = W )
(0). V is Subspace of W by RLSUB_1:39;
then the carrier of ((0). V) c= the carrier of W by RLSUB_1:def 2;
hence ((0). V) + W = W by Lm3; :: thesis: W + ((0). V) = W
hence W + ((0). V) = W by Lm1; :: thesis: verum