:: deftheorem Def6 defines |-- VECTSP_5:def 6 :
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v being Element of M
for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds
for b₆ being Element of [: the carrier of M, the carrier of M:] holds
( b₆ = v |-- (W1,W2) iff ( v = (b₆ `1) + (b<sub>6</sub> `2) & b₆ `1 in W1 & b<sub>6</sub> `2 in W2 ) );