theorem :: MATRLIN2:14

for K being Field
for V1 being finite-dimensional VectSp of K
for p being FinSequence of K
for B1 being FinSequence of V1
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
lmlt (p,B1) = lmlt (p,B2)