:: deftheorem Def8 defines AutMt ZMATRLIN:def 8 :
for V1, V2 being free finite-rank Z_Module
for f being Function of V1,V2
for b1 being FinSequence of V1
for b2 being OrdBasis of V2
for b₆ being Matrix of INT.Ring 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 ) ) );