theorem Th47: :: MATRLIN2:47

for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) & f is additive & f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2