let F be Field; :: thesis: for V, W being VectSp of F

for T being linear-transformation of V,W

for A being Subset of V

for B being Basis of V

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W

for A being Subset of V

for B being Basis of V

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let T be linear-transformation of V,W; :: thesis: for A being Subset of V

for B being Basis of V

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let A be Subset of V; :: thesis: for B being Basis of V

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let B be Basis of V; :: thesis: for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let l be Linear_Combination of B \ A; :: thesis: ( A is Basis of (ker T) & A c= B implies T . (Sum l) = Sum (T @ l) )

assume ( A is Basis of (ker T) & A c= B ) ; :: thesis: T . (Sum l) = Sum (T @ l)

then A1: T | (B \ A) is one-to-one by Th22;

Carrier l c= B \ A by VECTSP_6:def 4;

then A2: (T | (B \ A)) | (Carrier l) = T | (Carrier l) by RELAT_1:74;

then A3: T | (Carrier l) is one-to-one by A1, FUNCT_1:52;

consider G being FinSequence of V such that

A4: G is one-to-one and

A5: rng G = Carrier l and

A6: Sum l = Sum (l (#) G) by VECTSP_6:def 6;

set H = T * G;

reconsider H = T * G as FinSequence of W ;

A7: rng H = T .: (Carrier l) by A5, RELAT_1:127

.= Carrier (T @ l) by A3, Th39 ;

dom T = [#] V by Th7;

then H is one-to-one by A4, A5, A1, A2, Th1, FUNCT_1:52;

then A8: Sum (T @ l) = Sum ((T @ l) (#) H) by A7, VECTSP_6:def 6;

T * (l (#) G) = (T @ l) (#) H by A5, A3, Th38;

hence T . (Sum l) = Sum (T @ l) by A6, A8, MATRLIN:16; :: thesis: verum

for T being linear-transformation of V,W

for A being Subset of V

for B being Basis of V

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W

for A being Subset of V

for B being Basis of V

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let T be linear-transformation of V,W; :: thesis: for A being Subset of V

for B being Basis of V

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let A be Subset of V; :: thesis: for B being Basis of V

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let B be Basis of V; :: thesis: for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @ l)

let l be Linear_Combination of B \ A; :: thesis: ( A is Basis of (ker T) & A c= B implies T . (Sum l) = Sum (T @ l) )

assume ( A is Basis of (ker T) & A c= B ) ; :: thesis: T . (Sum l) = Sum (T @ l)

then A1: T | (B \ A) is one-to-one by Th22;

Carrier l c= B \ A by VECTSP_6:def 4;

then A2: (T | (B \ A)) | (Carrier l) = T | (Carrier l) by RELAT_1:74;

then A3: T | (Carrier l) is one-to-one by A1, FUNCT_1:52;

consider G being FinSequence of V such that

A4: G is one-to-one and

A5: rng G = Carrier l and

A6: Sum l = Sum (l (#) G) by VECTSP_6:def 6;

set H = T * G;

reconsider H = T * G as FinSequence of W ;

A7: rng H = T .: (Carrier l) by A5, RELAT_1:127

.= Carrier (T @ l) by A3, Th39 ;

dom T = [#] V by Th7;

then H is one-to-one by A4, A5, A1, A2, Th1, FUNCT_1:52;

then A8: Sum (T @ l) = Sum ((T @ l) (#) H) by A7, VECTSP_6:def 6;

T * (l (#) G) = (T @ l) (#) H by A5, A3, Th38;

hence T . (Sum l) = Sum (T @ l) by A6, A8, MATRLIN:16; :: thesis: verum