for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V
for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds
t = v |-- (W,L)