theorem ThComp1: :: ZMATRLIN:38

for V1, V2, V3 being free finite-rank Z_Module
for f being Function of V1,V2
for g being Function of V2,V3
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds
AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))