V is_the_direct_sum_of (0). V, (Omega). V by Th99, Th107;
then (Omega). V is with_Linear_Compl ;
hence ex b₁ being Submodule of V st b₁ is with_Linear_Compl ; :: thesis: verum