let V, W be Z_Module; :: thesis: 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; :: thesis: 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; :: thesis: for w being Element of W st w in Carrier (T @* l) holds
T " {w} meets Carrier l
let w be Element of W; :: thesis: ( w in Carrier (T @* l) implies T " {w} meets Carrier l )
assume w in Carrier (T @* l) ; :: thesis: T " {w} meets Carrier l
then A1: (T @* l) . w <> 0. INT.Ring by ZMODUL02:8;
assume A2: T " {w} misses Carrier l ; :: thesis: contradiction
(T " {w}) /\ (Carrier l) = {} by A2;
then L2: canFS ((T " {w}) /\ (Carrier l)) = <*> the carrier of INT.Ring ;
lCFST (l,T,w) = <*> the carrier of INT.Ring by L2;
then Sum (lCFST (l,T,w)) = 0. INT.Ring by RLVECT_1:43;
then Sum (lCFST (l,T,w)) = 0. INT.Ring ;
hence contradiction by A1, LDef5; :: thesis: verum