let F be Field; :: thesis: for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V holds im (canLinTrans f) = Lin (rng f)
let U be non trivial finite-dimensional VectSp of F; :: thesis: for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V holds im (canLinTrans f) = Lin (rng f)
let V be finite-dimensional VectSp of F; :: thesis: for B being Basis of U
for f being Function of B,V holds im (canLinTrans f) = Lin (rng f)
let B be Basis of U; :: thesis: for f being Function of B,V holds im (canLinTrans f) = Lin (rng f)
let f be Function of B,V; :: thesis: im (canLinTrans f) = Lin (rng f)
set T = canLinTrans f;
B: [#] (im (canLinTrans f)) = (canLinTrans f) .: ([#] U) by RANKNULL:def 2;
C: (canLinTrans f) .: ([#] U) is Subset of (im (canLinTrans f)) by RANKNULL:12;
G: ( the carrier of (Lin (rng f)) = { (Sum l) where l is Linear_Combination of rng f : verum } & the carrier of (Lin B) = { (Sum l) where l is Linear_Combination of B : verum } ) by VECTSP_7:def 2;
H: Lin B = ModuleStr(# the carrier of U, the addF of U, the ZeroF of U, the lmult of U #) by VECTSP_7:def 3;

F: now :: thesis: for o being object st o in the carrier of (im (canLinTrans f)) holds
o in the carrier of (Lin (rng f))

let o be object ; :: thesis: ( o in the carrier of (im (canLinTrans f)) implies o in the carrier of (Lin (rng f)) )
assume o in the carrier of (im (canLinTrans f)) ; :: thesis: o in the carrier of (Lin (rng f))
then consider u being object such that
F1: ( u in dom (canLinTrans f) & u in [#] U & o = (canLinTrans f) . u ) by B, FUNCT_1:def 6;
reconsider u = u as Element of U by F1;
u in Lin B by H;
then consider l being Linear_Combination of B such that
F2: Sum l = u by G;
(canLinTrans f) .: B c= rng f by canlinsurj2;
then o in Lin (rng f) by F1, F2, canlinsurj1;
hence o in the carrier of (Lin (rng f)) ; :: thesis: verum

end;

now :: thesis: for o being object st o in the carrier of (Lin (rng f)) holds
o in the carrier of (im (canLinTrans f))

let o be object ; :: thesis: ( o in the carrier of (Lin (rng f)) implies o in the carrier of (im (canLinTrans f)) )
assume o in the carrier of (Lin (rng f)) ; :: thesis: o in the carrier of (im (canLinTrans f))
then consider l2 being Linear_Combination of rng f such that
G1: o = Sum l2 by G;
consider l1 being Linear_Combination of B such that
G2: (canLinTrans f) . (Sum l1) = Sum l2 by canlinsurj3;
dom (canLinTrans f) = the carrier of U by FUNCT_2:def 1;
then Sum l2 in (canLinTrans f) .: ([#] U) by G2, FUNCT_1:def 6;
hence o in the carrier of (im (canLinTrans f)) by G1, C; :: thesis: verum

end;

hence im (canLinTrans f) = Lin (rng f) by F, TARSKI:2, VECTSP_4:29; :: thesis: verum