:: deftheorem Def8 defines AutMt MATRLIN:def 8 :
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being FinSequence of V1
for b2 being OrdBasis of V2
for b₇ being Matrix of K holds
( b₇ = AutMt (f,b1,b2) iff ( len b₇ = len b1 & ( for k being Nat st k in dom b1 holds
b₇ /. k = (f . (b1 /. k)) |-- b2 ) ) );