let F be Field; :: thesis: for U, V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V holds (canLinTrans f) .: B c= rng f
let U, V be finite-dimensional VectSp of F; :: thesis: for B being Basis of U
for f being Function of B,V holds (canLinTrans f) .: B c= rng f
let B be Basis of U; :: thesis: for f being Function of B,V holds (canLinTrans f) .: B c= rng f
let f be Function of B,V; :: thesis: (canLinTrans f) .: B c= rng f
set T = canLinTrans f;

now :: thesis: for o being object st o in (canLinTrans f) .: B holds
o in rng f

let o be object ; :: thesis: ( o in (canLinTrans f) .: B implies o in rng f )
assume o in (canLinTrans f) .: B ; :: thesis: o in rng f
then consider x being object such that
A: ( x in dom (canLinTrans f) & x in B & o = (canLinTrans f) . x ) by FUNCT_1:def 6;
B: dom f = B by FUNCT_2:def 1;
f . x = ((canLinTrans f) | B) . x by defcl
.= (canLinTrans f) . x by A, FUNCT_1:49 ;
hence o in rng f by A, B, FUNCT_1:3; :: thesis: verum

end;

hence (canLinTrans f) .: B c= rng f ; :: thesis: verum