let F be Field; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V
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 l being Linear_Combination of V
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 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 A1: w in Carrier (T @ l) ; :: thesis: T " {w} meets Carrier l
A2: (T @ l) . w <> 0. F by A1, VECTSP_6:20;
assume A3: T " {w} misses Carrier l ; :: thesis: contradiction

per cases ( T " {w} = {} or T " {w} <> {} ) ;

suppose T " {w} = {} ; :: thesis: contradiction

then Sum (l .: (T " {w})) = Sum ({} F) by RELAT_1:149
.= 0. F by RLVECT_2:14 ;
hence contradiction by A2, Def5; :: thesis: verum

end;

suppose T " {w} <> {} ; :: thesis: contradiction

then l .: (T " {w}) = {(0. F)} by A3, Th35;
then Sum (l .: (T " {w})) = 0. F by RLVECT_2:15;
hence contradiction by A2, Def5; :: thesis: verum

end;

end;