let K be Field; :: thesis: for V, W being VectSp of K
for T being linear-transformation of V,W
for A being Subset of V
for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
let V, W be VectSp of K; :: thesis: for T being linear-transformation of V,W
for A being Subset of V
for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
let T be linear-transformation of V,W; :: thesis: for A being Subset of V
for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
let A be Subset of V; :: thesis: for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
let L be Linear_Combination of A; :: thesis: ( T | A is one-to-one implies T . (Sum L) = Sum (T @ L) )
consider G being FinSequence of V such that
A1: G is one-to-one and
A2: rng G = Carrier L and
A3: Sum L = Sum (L (#) G) by VECTSP_6:def 6;
set H = T * G;
reconsider H = T * G as FinSequence of W ;
Carrier L c= A by VECTSP_6:def 4;
then A4: (T | A) | (Carrier L) = T | (Carrier L) by RELAT_1:74;
assume A5: T | A is one-to-one ; :: thesis: T . (Sum L) = Sum (T @ L)
then A6: T | (Carrier L) is one-to-one by A4, FUNCT_1:52;
A7: rng H = T .: (Carrier L) by A2, RELAT_1:127
.= Carrier (T @ L) by A6, RANKNULL:39 ;
dom T = [#] V by FUNCT_2:def 1;
then H is one-to-one by A5, A4, A1, A2, FUNCT_1:52, RANKNULL:1;
then A8: Sum (T @ L) = Sum ((T @ L) (#) H) by A7, VECTSP_6:def 6;
T * (L (#) G) = (T @ L) (#) H by A6, A2, RANKNULL:38;
hence T . (Sum L) = Sum (T @ L) by A3, A8, MATRLIN:16; :: thesis: verum