let F be Field; :: thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
let W, V be VectSp of F; :: thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
let T be linear-transformation of V,W; :: thesis: for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
let l be Linear_Combination of V; :: thesis: ( T | (Carrier l) is one-to-one implies T .: (Carrier l) = Carrier (T @ l) )
assume A1: T | (Carrier l) is one-to-one ; :: thesis: T .: (Carrier l) = Carrier (T @ l)
A2: Carrier (T @ l) c= T .: (Carrier l) by Th30;
T .: (Carrier l) c= Carrier (T @ l)

proof

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in T .: (Carrier l) or w in Carrier (T @ l) )
assume A3: w in T .: (Carrier l) ; :: thesis: w in Carrier (T @ l)
consider v being set such that
A4: v in dom T and
A5: v in Carrier l and
A6: T . v = w by A3, FUNCT_1:def 12;
reconsider v = v as Element of V by A4;
A7: (T @ l) . (T . v) = l . v by A1, A5, Th37;
l . v <> 0. F by A5, VECTSP_6:20;
hence w in Carrier (T @ l) by A6, A7; :: thesis: verum

end;

hence T .: (Carrier l) = Carrier (T @ l) by A2, XBOOLE_0:def 10; :: thesis: verum