let F be Field; :: thesis: for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2 being Linear_Combination of B
for a being Element of F st a * l1 = l2 holds
Sum (f (#) l2) = a * (Sum (f (#) l1))
let U, V be VectSp of F; :: thesis: for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2 being Linear_Combination of B
for a being Element of F st a * l1 = l2 holds
Sum (f (#) l2) = a * (Sum (f (#) l1))
let B be non empty finite Subset of U; :: thesis: for f being Function of B,V
for l1, l2 being Linear_Combination of B
for a being Element of F st a * l1 = l2 holds
Sum (f (#) l2) = a * (Sum (f (#) l1))
let f be Function of B,V; :: thesis: for l1, l2 being Linear_Combination of B
for a being Element of F st a * l1 = l2 holds
Sum (f (#) l2) = a * (Sum (f (#) l1))
let l1, l2 be Linear_Combination of B; :: thesis: for a being Element of F st a * l1 = l2 holds
Sum (f (#) l2) = a * (Sum (f (#) l1))
let a be Element of F; :: thesis: ( a * l1 = l2 implies Sum (f (#) l2) = a * (Sum (f (#) l1)) )
assume l2 = a * l1 ; :: thesis: Sum (f (#) l2) = a * (Sum (f (#) l1))
then f (#) l2 = a * (f (#) l1) by lemmultx;
hence Sum (f (#) l2) = a * (Sum (f (#) l1)) by VECTSP_6:45; :: thesis: verum