for F being Field
for X, Y being VectSp of F
for l being Linear_Combination of X
for T being linear-transformation of X,Y st T is one-to-one holds
T @ l = T @* l