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 st T | (Carrier l) is one-to-one holds

T .: (Carrier l) = Carrier (T @ l)

let V, W 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: T .: (Carrier l) c= Carrier (T @ l)

hence T .: (Carrier l) = Carrier (T @ l) by A2; :: thesis: verum

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 V, W 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: T .: (Carrier l) c= Carrier (T @ l)

proof

Carrier (T @ l) c= T .: (Carrier l)
by Th30;
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. F ) by A1, A4, Th37, VECTSP_6:2;

hence w in Carrier (T @ l) by A5; :: thesis: verum

end;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. F ) by A1, A4, Th37, VECTSP_6:2;

hence w in Carrier (T @ l) by A5; :: thesis: verum

hence T .: (Carrier l) = Carrier (T @ l) by A2; :: thesis: verum