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

A3: b1 is one-to-one by MATRLIN:def 4;
reconsider R = rng b1 as Basis of V1 by MATRLIN:def 4;
let x be set ; :: 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
X: Seg (len b1) = {} by A2;
dim V1 = card R by VECTSP_9:def 2
.= card (dom b1) by A3, POLYFORM:2
.= 0 by X, CARD_1:47, 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 A4, 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 3
.= 0. V2 by VECTSP_1:60
.= (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:18; :: thesis: verum

end;

suppose A5: 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 ;
A6: rng b1 is Subset of V1 by FINSEQ_1:def 4;
dom f = the carrier of V1 by FUNCT_2:def 1;
then A7: len fb = len b1 by A6, FINSEQ_2:33;
dom (Mx2Tran (AutMt f,b1,b2),b1,b2) = the carrier of V1 by FUNCT_2:def 1;
then A8: len Mf = len b1 by A6, FINSEQ_2:33;

now

A9: dom fb = dom Mf by A7, A8, FINSEQ_3:31;
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 A10: i in dom fb by FINSEQ_3:27;
dom fb = dom b1 by A7, FINSEQ_3:31;
then A11: b1 . i = b1 /. i by A10, 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, A11, FUNCT_1:22
.= Mf . i by A10, A9, A11, FUNCT_1:22 ;
:: thesis: verum

end;

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

end;

end;