:: deftheorem defines HIPERPLANE LMOD_7:def 5 :
for K being Ring
for V being LeftMod of K st not V is trivial & V is free holds
for b₃ being strict Subspace of V holds
( b₃ is HIPERPLANE of V iff ex a being Vector of V st
( a <> 0. V & V is_the_direct_sum_of <:a:>,b₃ ) );