consider C being strict Subspace of V such that

A1: V is_the_direct_sum_of C,W by Lm15;

C is Linear_Compl of W by A1, Def5;

hence ex b_{1} being Linear_Compl of W st b_{1} is strict
; :: thesis: verum

A1: V is_the_direct_sum_of C,W by Lm15;

C is Linear_Compl of W by A1, Def5;

hence ex b