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 Carrier (T @ l) c= 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 Carrier (T @ l) c= T .: (Carrier l)
let T be linear-transformation of V,W; :: thesis: for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
let l be Linear_Combination of V; :: thesis: Carrier (T @ l) c= T .: (Carrier l)
T @ l is Linear_Combination of T .: (Carrier l) by Th29;
hence Carrier (T @ l) c= T .: (Carrier l) by VECTSP_6:def 4; :: thesis: verum