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
f (#) l3 = (f (#) l1) - (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
f (#) l3 = (f (#) l1) - (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
f (#) l3 = (f (#) l1) - (f (#) l2)
let f be Function of B,V; :: thesis: for l1, l2, l3 being Linear_Combination of B st l3 = l1 - l2 holds
f (#) l3 = (f (#) l1) - (f (#) l2)
let l1, l2, l3 be Linear_Combination of B; :: thesis: ( l3 = l1 - l2 implies f (#) l3 = (f (#) l1) - (f (#) l2) )
assume A: l3 = l1 - l2 ; :: thesis: f (#) l3 = (f (#) l1) - (f (#) l2)
reconsider l4 = - l2 as Linear_Combination of B by VECTSP_6:39;
B: - (f (#) l2) = f (#) l4 by lemmultx;
thus f (#) l3 = (f (#) l1) - (f (#) l2) by A, B, lemaddx; :: thesis: verum