for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )