ex C being strict Subspace of V st V is_the_direct_sum_of C,W by Lm14;
hence ex b₁ being Subspace of V st V is_the_direct_sum_of b₁,W ; :: thesis: verum