:: deftheorem LDef5 defines @* ZMODUL05:def 8 :
for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for b₆ being Linear_Combination of W holds
( b₆ = T @* l iff ( Carrier b₆ c= T .: (Carrier l) & ( for w being Element of W holds b₆ . w = Sum (lCFST (l,T,w)) ) ) );