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, l3 being Linear_Combination of B st l3 = l1 + l2 holds
Sum (f (#) l3) = (Sum (f (#) l1)) + (Sum (f (#) l2))
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, l3 being Linear_Combination of B st l3 = l1 + l2 holds
Sum (f (#) l3) = (Sum (f (#) l1)) + (Sum (f (#) l2))
let B be non empty finite Subset of U; :: thesis: for f being Function of B,V
for l1, l2, l3 being Linear_Combination of B st l3 = l1 + l2 holds
Sum (f (#) l3) = (Sum (f (#) l1)) + (Sum (f (#) l2))
let f be Function of B,V; :: thesis: for l1, l2, l3 being Linear_Combination of B st l3 = l1 + l2 holds
Sum (f (#) l3) = (Sum (f (#) l1)) + (Sum (f (#) l2))
let l1, l2, l3 be Linear_Combination of B; :: thesis: ( l3 = l1 + l2 implies Sum (f (#) l3) = (Sum (f (#) l1)) + (Sum (f (#) l2)) )
assume l3 = l1 + l2 ; :: thesis: Sum (f (#) l3) = (Sum (f (#) l1)) + (Sum (f (#) l2))
then f (#) l3 = (f (#) l1) + (f (#) l2) by lemaddx;
hence Sum (f (#) l3) = (Sum (f (#) l1)) + (Sum (f (#) l2)) by VECTSP_6:44; :: thesis: verum