consider C being strict Subspace of V such that
A1: V is_the_direct_sum_of C,W by Lm14;
C is Linear_Compl of W by A1, Def5;
hence ex b₁ being Linear_Compl of W st b₁ is strict ; :: thesis: verum