:: deftheorem defines COMPL LMOD_7:def 16 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b₄ being UnOp of (V .. W) holds
( b₄ = COMPL W iff for S1 being Element of V .. W holds b₄ . S1 = - S1 );