theorem Th36: :: RLSUB_2:36

for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & L + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) )