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 st f is linear holds
Mx2Tran (AutMt f,b1,b2),b1,b2 = f
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 st f is linear holds
Mx2Tran (AutMt f,b1,b2),b1,b2 = f
let f be Function of V1,V2; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st f is linear holds
Mx2Tran (AutMt f,b1,b2),b1,b2 = f
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2 st f is linear holds
Mx2Tran (AutMt f,b1,b2),b1,b2 = f
let b2 be OrdBasis of V2; :: thesis: ( f is linear implies Mx2Tran (AutMt f,b1,b2),b1,b2 = f )
assume A1: f is linear ; :: thesis: Mx2Tran (AutMt f,b1,b2),b1,b2 = f
set A = AutMt f,b1,b2;
set M = Mx2Tran (AutMt f,b1,b2),b1,b2;

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

suppose A2: len b1 = 0 ; :: thesis: Mx2Tran (AutMt f,b1,b2),b1,b2 = f

now

let x be set ; :: thesis: ( x in the carrier of V1 implies f . x = (Mx2Tran (AutMt f,b1,b2),b1,b2) . x )
assume A3: x in the carrier of V1 ; :: thesis: f . x = (Mx2Tran (AutMt f,b1,b2),b1,b2) . x
reconsider R = rng b1 as Basis of V1 by MATRLIN:def 4;
A4: b1 is one-to-one by MATRLIN:def 4;
dim V1 = card R by VECTSP_9:def 2
.= card (dom b1) by A4, POLYFORM:2
.= 0 by A2, CARD_1:47, FINSEQ_1:4, FINSEQ_1:def 3 ;
then (Omega). V1 = (0). V1 by VECTSP_9:33;
then the carrier of V1 = {(0. V1)} by VECTSP_4:def 3;
then x = 0. V1 by A3, TARSKI:def 1;
hence f . x = f . ((0. K) * (0. V1)) by VECTSP_1:60
.= (0. K) * (f . (0. V1)) by A1, MOD_2:def 5
.= 0. V2 by VECTSP_1:60
.= (Mx2Tran (AutMt f,b1,b2),b1,b2) . x by A2, A3, Th33 ;
:: thesis: verum

end;

hence Mx2Tran (AutMt f,b1,b2),b1,b2 = f by FUNCT_2:18; :: thesis: verum

end;

suppose A5: len b1 > 0 ; :: thesis: Mx2Tran (AutMt f,b1,b2),b1,b2 = f

A6: ( dom (Mx2Tran (AutMt f,b1,b2),b1,b2) = the carrier of V1 & dom f = the carrier of V1 & rng b1 is Subset of V1 ) by FINSEQ_1:def 4, FUNCT_2:def 1;
reconsider fb = f * b1, Mf = (Mx2Tran (AutMt f,b1,b2),b1,b2) * b1 as FinSequence ;
A7: ( len fb = len b1 & len Mf = len b1 ) by A6, FINSEQ_2:33;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len fb implies fb . i = Mf . i )
assume A8: ( 1 <= i & i <= len fb ) ; :: thesis: fb . i = Mf . i
A9: ( i in dom fb & dom fb = dom b1 & dom fb = dom Mf ) by A7, A8, FINSEQ_3:27, FINSEQ_3:31;
then A10: b1 . i = b1 /. i by PARTFUN1:def 8;
LineVec2Mx (((Mx2Tran (AutMt f,b1,b2),b1,b2) . (b1 /. i)) |-- b2) = (LineVec2Mx ((b1 /. i) |-- b1)) * (AutMt f,b1,b2) by A5, Th32
.= LineVec2Mx ((f . (b1 /. i)) |-- b2) by A1, A5, Th31 ;
then ((Mx2Tran (AutMt f,b1,b2),b1,b2) . (b1 /. i)) |-- b2 = Line (LineVec2Mx ((f . (b1 /. i)) |-- b2)),1 by MATRIX15:25
.= (f . (b1 /. i)) |-- b2 by MATRIX15:25 ;
then (Mx2Tran (AutMt f,b1,b2),b1,b2) . (b1 /. i) = f . (b1 /. i) by MATRLIN:39;
hence fb . i = (Mx2Tran (AutMt f,b1,b2),b1,b2) . (b1 /. i) by A10, A9, FUNCT_1:22
.= Mf . i by A10, A9, FUNCT_1:22 ;
:: thesis: verum

end;

then Mf = fb by A7, FINSEQ_1:18;
hence Mx2Tran (AutMt f,b1,b2),b1,b2 = f by A1, A5, MATRLIN:26; :: thesis: verum

end;

end;