:: deftheorem Def6 defines |-- RLSUB_2:def 6 :
for V being RealLinearSpace
for v being VECTOR of V
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for b₅ being Element of [: the carrier of V, the carrier of V:] holds
( b₅ = v |-- (W1,W2) iff ( v = (b₅ `1) + (b<sub>5</sub> `2) & b₅ `1 in W1 & b<sub>5</sub> `2 in W2 ) );