:: deftheorem defines ! ZMODUL05:def 6 :
for R being Ring
for V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V holds l ! A = (l | A) +* ((A `) --> (0. R));