let K be Field; :: thesis: for V2, V1 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 linear holds
(Mx2Tran A,b1,M) . v1 = (f . v1) |-- b2
let V2, V1 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 linear 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 linear 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 linear 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 linear 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 linear 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 linear 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 linear 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 linear implies (Mx2Tran A,b1,M) . v1 = (f . v1) |-- b2 )
assume A2: ( A = AutMt f,b1,b2 & f is linear ) ; :: thesis: (Mx2Tran A,b1,M) . v1 = (f . v1) |-- b2
reconsider f' = f as linear-transformation of V1,V2 by A2;
set MM = Mx2Tran A,b1,M;

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

suppose A3: 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:33;
then A4: the carrier of V1 = {(0. V1)} by VECTSP_4:def 3;
v1 = 0. V1 by A4, TARSKI:def 1;
then v1 in ker f' 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 Th33, A3 ;
:: 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, 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;