:: deftheorem LDef5 defines @* ZMODUL05:def 8 :
for V, W being Z_Module
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)) ) ) );