let F be Field; :: thesis: for V, W 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 V, W 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 object ; :: 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:2;

now :: thesis: not T " {w} misses Carrier l

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:8; :: thesis: verum

end;

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

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {(0. F)} or y in l .: (T " {w}) )
assume y in {(0. F)} ; :: thesis: y in l .: (T " {w})
then A7: y = 0. F by TARSKI:def 1;
ex z being object st z in l .: (T " {w}) by A5, XBOOLE_0:def 1;
hence y in l .: (T " {w}) by A4, A7, TARSKI:def 1; :: thesis: verum

end;

l .: (T " {w}) c= {(0. F)} by A3, Th28;
then l .: (T " {w}) = {(0. F)} by A6;
hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:9; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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