:: deftheorem Def5 defines Linear_Compl VECTSP_5:def 5 :
for F being Field
for V being VectSp of F
for W, b₄ being Subspace of V holds
( b₄ is Linear_Compl of W iff V is_the_direct_sum_of b₄,W );