theorem :: RANKNULL:23

for F being Field
for V being VectSp of F
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}