let F be Field; :: thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
let W, V be VectSp of F; :: thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
let T be linear-transformation of V,W; :: thesis: for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
let l be Linear_Combination of V; :: thesis: T @ l is Linear_Combination of T .: (Carrier l)
Carrier (T @ l) c= T .: (Carrier l)

proof

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in Carrier (T @ l) or w in T .: (Carrier l) )
assume A1: w in Carrier (T @ l) ; :: thesis: w in T .: (Carrier l)
reconsider w = w as Element of W by A1;
A2: (T @ l) . w <> 0. F by A1, VECTSP_6:20;

now

assume A3: T " {w} misses Carrier l ; :: thesis: contradiction
then A4: l .: (T " {w}) c= {(0. F)} by Th28;
Sum (l .: (T " {w})) = 0. F

proof

per cases ( l .: (T " {w}) = {} F or l .: (T " {w}) <> {} F ) ;

suppose l .: (T " {w}) = {} F ; :: thesis: Sum (l .: (T " {w})) = 0. F

hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:14; :: thesis: verum

end;

suppose A5: l .: (T " {w}) <> {} F ; :: thesis: Sum (l .: (T " {w})) = 0. F

l .: (T " {w}) = {(0. F)}

proof

thus l .: (T " {w}) c= {(0. F)} by A3, Th28; :: according to XBOOLE_0:def 10 :: thesis: {(0. F)} c= l .: (T " {w})
thus {(0. F)} c= l .: (T " {w}) :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {(0. F)} or y in l .: (T " {w}) )
assume A6: y in {(0. F)} ; :: thesis: y in l .: (T " {w})
A7: y = 0. F by A6, TARSKI:def 1;
consider z being set such that
A8: z in l .: (T " {w}) by A5, XBOOLE_0:def 1;
thus y in l .: (T " {w}) by A4, A7, A8, TARSKI:def 1; :: thesis: verum

end;

end;

hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:15; :: thesis: verum

end;

end;

end;

hence contradiction by A2, Def5; :: thesis: verum

end;

then consider x being set such that
A9: x in T " {w} and
A10: x in Carrier l by XBOOLE_0:3;
A11: x in dom T by A9, FUNCT_1:def 13;
A12: T . x in {w} by A9, FUNCT_1:def 13;
reconsider x = x as Element of V by A9;
T . x = w by A12, TARSKI:def 1;
hence w in T .: (Carrier l) by A10, A11, FUNCT_1:def 12; :: thesis: verum

end;

hence T @ l is Linear_Combination of T .: (Carrier l) by VECTSP_6:def 7; :: thesis: verum