let F be Field; :: thesis: for V being VectSp of F holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
let V be VectSp of F; :: thesis: ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) by Th52;
hence ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Def5; :: thesis: verum