let F be Field; :: thesis: for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of rng f holds (canLinTrans f) . (Sum (l (#) f)) = Sum l
let U be non trivial finite-dimensional VectSp of F; :: thesis: for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of rng f holds (canLinTrans f) . (Sum (l (#) f)) = Sum l
let V be finite-dimensional VectSp of F; :: thesis: for B being Basis of U
for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of rng f holds (canLinTrans f) . (Sum (l (#) f)) = Sum l
let B be Basis of U; :: thesis: for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of rng f holds (canLinTrans f) . (Sum (l (#) f)) = Sum l
let f be Function of B,V; :: thesis: ( f is one-to-one implies for l being Linear_Combination of rng f holds (canLinTrans f) . (Sum (l (#) f)) = Sum l )
assume AS: f is one-to-one ; :: thesis: for l being Linear_Combination of rng f holds (canLinTrans f) . (Sum (l (#) f)) = Sum l
let l be Linear_Combination of rng f; :: thesis: (canLinTrans f) . (Sum (l (#) f)) = Sum l
(canLinTrans f) . (Sum (l (#) f)) = Sum (f (#) (l (#) f)) by CLS;
hence (canLinTrans f) . (Sum (l (#) f)) = Sum l by AS, XXX4; :: thesis: verum