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 additive & f is homogeneous 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 additive & f is homogeneous 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 additive & f is homogeneous 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 additive & f is homogeneous holds
Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f
let b2 be OrdBasis of V2; :: thesis: ( f is additive & f is homogeneous implies Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f )
assume A1: ( f is additive & f is homogeneous ) ; :: 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 :: thesis: for x being object st x in the carrier of V1 holds
f . x = (Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . x

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

end;

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

end;

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

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

now :: thesis: for i being Nat st 1 <= i & i <= len fb holds
fb . i = Mf . i

A10: dom fb = dom Mf by A8, A9, FINSEQ_3:29;
let i be Nat; :: thesis: ( 1 <= i & i <= len fb implies fb . i = Mf . i )
assume ( 1 <= i & i <= len fb ) ; :: thesis: fb . i = Mf . i
then A11: i in dom fb by FINSEQ_3:25;
dom fb = dom b1 by A8, FINSEQ_3:29;
then A12: b1 . i = b1 /. i by A11, PARTFUN1:def 6;
LineVec2Mx (((Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . (b1 /. i)) |-- b2) = (LineVec2Mx ((b1 /. i) |-- b1)) * (AutMt (f,b1,b2)) by A6, Th32
.= LineVec2Mx ((f . (b1 /. i)) |-- b2) by A1, A6, 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:34;
hence fb . i = (Mx2Tran ((AutMt (f,b1,b2)),b1,b2)) . (b1 /. i) by A11, A12, FUNCT_1:12
.= Mf . i by A11, A10, A12, FUNCT_1:12 ;
:: thesis: verum

end;

hence Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f by A1, A6, A8, A9, FINSEQ_1:14, MATRLIN:22; :: thesis: verum

end;

end;