for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L ) by Def5, Lm17;