theorem canlinsurj2: :: VECTSP13:19

for F being Field
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