:: deftheorem Def5 defines @ RANKNULL:def 5 :
for F being Field
for V, W being VectSp of F
for l being Linear_Combination of V
for T being linear-transformation of V,W
for b₆ being Linear_Combination of W holds
( b₆ = T @ l iff for w being Element of W holds b₆ . w = Sum (l .: (T " {w})) );