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

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

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

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

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

end;

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

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

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in {(0. F)} ; :: thesis:
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:

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:

end;

end;

end;

hence contradiction by A2, Def5; :: thesis:

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:

end;

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