( ((0). V) + ((Omega). V) = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & (0). V = ((0). V) /\ ((Omega). V) ) by Th99, Th107;
then V is_the_direct_sum_of (0). V, (Omega). V by Def17;
then (Omega). V is with_Linear_Compl by Def18;
hence ex b₁ being Submodule of V st b₁ is with_Linear_Compl ; :: thesis: verum