let R be Ring; :: thesis: for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @* l)
let V, W be LeftMod of R; :: thesis: for l being Linear_Combination of V
for T being linear-transformation of V,W st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @* l)
let l be Linear_Combination of V; :: thesis: for T being linear-transformation of V,W st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @* l)
let T be linear-transformation of V,W; :: 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: T .: (Carrier l) c= Carrier (T @* l)

proof

let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in T .: (Carrier l) or w in Carrier (T @* l) )
assume w in T .: (Carrier l) ; :: thesis: w in Carrier (T @* l)
then consider v being object such that
A3: v in dom T and
A4: v in Carrier l and
A5: T . v = w by FUNCT_1:def 6;
reconsider v = v as Element of V by A3;
( (T @* l) . (T . v) = l . v & l . v <> 0. R ) by A1, A4, Th37, ZMODUL02:8;
hence w in Carrier (T @* l) by A5; :: thesis: verum

end;

thus T .: (Carrier l) = Carrier (T @* l) by LDef5, A2; :: thesis: verum