for V being RealUnitarySpace
for W being Subspace of V
for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )