:: deftheorem Def5 defines |-- RMOD_3:def 5 :
for R being Ring
for V being RightMod of R
for v being Vector of V
for W1, W2 being Submodule 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>6</sub> `2) & b₆ `1 in W1 & b<sub>6</sub> `2 in W2 ) );