let R be Ring; for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for w being Element of W st w in Carrier (T @* l) holds
T " {w} meets Carrier l
let V, W be LeftMod of R; for l being Linear_Combination of V
for T being linear-transformation of V,W
for w being Element of W st w in Carrier (T @* l) holds
T " {w} meets Carrier l
let l be Linear_Combination of V; for T being linear-transformation of V,W
for w being Element of W st w in Carrier (T @* l) holds
T " {w} meets Carrier l
let T be linear-transformation of V,W; for w being Element of W st w in Carrier (T @* l) holds
T " {w} meets Carrier l
let w be Element of W; ( w in Carrier (T @* l) implies T " {w} meets Carrier l )
assume
w in Carrier (T @* l)
; T " {w} meets Carrier l
then A1:
(T @* l) . w <> 0. R
by ZMODUL02:8;
assume
T " {w} misses Carrier l
; contradiction
then
lCFST (l,T,w) = <*> the carrier of R
;
then
Sum (lCFST (l,T,w)) = 0. R
by RLVECT_1:43;
hence
contradiction
by A1, LDef5; verum