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 w in Carrier (T @ l) ; :: thesis: T " {w} meets Carrier l

then A1: (T @ l) . w <> 0. F by VECTSP_6:2;

assume A2: T " {w} misses Carrier l ; :: thesis: contradiction

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 w in Carrier (T @ l) ; :: thesis: T " {w} meets Carrier l

then A1: (T @ l) . w <> 0. F by VECTSP_6:2;

assume A2: T " {w} misses Carrier l ; :: thesis: contradiction