for a being Real
for i being Integer
for V being RealLinearSpace
for A being Subset of V
for l being Linear_Combination of A st a = i holds
a * l = i * l