:: deftheorem defcl defines canLinTrans VECTSP13:def 4 :
for F being Field
for U being finite-dimensional VectSp of F
for V being VectSp of F
for B being Basis of U
for f being Function of B,V
for b₆ being linear-transformation of U,V holds
( b₆ = canLinTrans f iff b₆ | B = f );