:: deftheorem Def6 defines # RANKNULL:def 6 :
for F being Field
for V, W being VectSp of F
for X being Subset of V
for T being linear-transformation of V,W
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T # l = (l * T) +* ((V \ X) --> (0. F));