for a being Element of INT.Ring
for V1, V2 being free finite-rank Z_Module
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st a <> 0. INT.Ring holds
AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))