:: deftheorem defines ! RANKNULL:def 4 :
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V holds l ! A = (l | A) +* ((V \ A) --> (0. F));