let a be Real; :: thesis: 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
let i be Integer; :: thesis: 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
let V be RealLinearSpace; :: thesis: for A being Subset of V
for l being Linear_Combination of A st a = i holds
a * l = i * l
let A be Subset of V; :: thesis: for l being Linear_Combination of A st a = i holds
a * l = i * l
let l be Linear_Combination of A; :: thesis: ( a = i implies a * l = i * l )
assume A1: a = i ; :: thesis: a * l = i * l
for v being VECTOR of V holds (i * l) . v = a * (l . v) by A1, Def1;
hence a * l = i * l by RLVECT_2:def 11; :: thesis: verum