let R be Ring; :: thesis: for V, W being LeftMod of R

for l being Linear_Combination of V

for T being linear-transformation of V,W holds T @* l is Linear_Combination of T .: (Carrier l)

let V, W be LeftMod of R; :: thesis: for l being Linear_Combination of V

for T being linear-transformation of V,W holds T @* l is Linear_Combination of T .: (Carrier l)

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

let T be linear-transformation of V,W; :: thesis: T @* l is Linear_Combination of T .: (Carrier l)

Carrier (T @* l) c= T .: (Carrier l) by LDef5;

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

for l being Linear_Combination of V

for T being linear-transformation of V,W holds T @* l is Linear_Combination of T .: (Carrier l)

let V, W be LeftMod of R; :: thesis: for l being Linear_Combination of V

for T being linear-transformation of V,W holds T @* l is Linear_Combination of T .: (Carrier l)

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

let T be linear-transformation of V,W; :: thesis: T @* l is Linear_Combination of T .: (Carrier l)

Carrier (T @* l) c= T .: (Carrier l) by LDef5;

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