let K be Field; :: thesis: 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
let V1, V2 be finite-dimensional VectSp of K; :: thesis: 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
let f be Function of V1,V2; :: thesis: 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
let b1 be OrdBasis of V1; :: thesis: 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
let b2 be OrdBasis of V2; :: thesis: 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
let v1 be Element of V1; :: thesis: 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
let M be OrdBasis of (len b2) -VectSp_over K; :: thesis: ( M = MX2FinS (1. (K,(len b2))) implies 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 )
assume A1: M = MX2FinS (1. (K,(len b2))) ; :: thesis: 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
let A be Matrix of len b1, len M,K; :: thesis: ( A = AutMt (f,b1,b2) & f is additive & f is homogeneous implies (Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2 )
assume that
A2: A = AutMt (f,b1,b2) and
A3: ( f is additive & f is homogeneous ) ; :: thesis: (Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
reconsider f9 = f as linear-transformation of V1,V2 by A3;
set MM = Mx2Tran (A,b1,M);

per cases ( len b1 = 0 or len b1 > 0 ) ;

suppose A4: len b1 = 0 ; :: thesis: (Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2

then dim V1 = 0 by Th21;
then (Omega). V1 = (0). V1 by VECTSP_9:29;
then the carrier of V1 = {(0. V1)} by VECTSP_4:def 3;
then v1 = 0. V1 by TARSKI:def 1;
then v1 in ker f9 by RANKNULL:11;
hence (f . v1) |-- b2 = (0. V2) |-- b2 by RANKNULL:10
.= (len b2) |-> (0. K) by Th20
.= 0. ((len b2) -VectSp_over K) by MATRIX13:102
.= (Mx2Tran (A,b1,M)) . v1 by A4, Th33 ;
:: thesis: verum

end;

suppose A5: len b1 > 0 ; :: thesis: (Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2

then LineVec2Mx (((Mx2Tran (A,b1,M)) . v1) |-- M) = (LineVec2Mx (v1 |-- b1)) * A by Th32
.= LineVec2Mx ((f . v1) |-- b2) by A2, A3, A5, Th31 ;
hence (f . v1) |-- b2 = Line ((LineVec2Mx (((Mx2Tran (A,b1,M)) . v1) |-- M)),1) by MATRIX15:25
.= ((Mx2Tran (A,b1,M)) . v1) |-- M by MATRIX15:25
.= (Mx2Tran (A,b1,M)) . v1 by A1, Th46 ;
:: thesis: verum

end;

end;