let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for M being Matrix of len b1, len b2,K holds AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for M being Matrix of len b1, len b2,K holds AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for M being Matrix of len b1, len b2,K holds AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
let b2 be OrdBasis of V2; :: thesis: for M being Matrix of len b1, len b2,K holds AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
let M be Matrix of len b1, len b2,K; :: thesis: AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
set MX = Mx2Tran (M,b1,b2);
set A = AutMt ((Mx2Tran (M,b1,b2)),b1,b2);
set ONE = 1. (K,(len b1));
A1: len M = len b1 by MATRIX_0:25;
A2: len (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) = len b1 by MATRIX_0:25;
A3: len (1. (K,(len b1))) = len b1 by MATRIX_0:24;

now :: thesis: for i being Nat st 1 <= i & i <= len M holds
M . i = (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len M implies M . i = (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) . i )
assume A4: ( 1 <= i & i <= len M ) ; :: thesis: M . i = (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) . i
A5: i in Seg (len b1) by A1, A4;
A6: i in dom (1. (K,(len b1))) by A1, A3, A4, FINSEQ_3:25;
reconsider Ai = (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) /. i as FinSequence of K by FINSEQ_1:def 11;
A7: i in dom b1 by A1, A4, FINSEQ_3:25;
then (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) /. i = ((Mx2Tran (M,b1,b2)) . (b1 /. i)) |-- b2 by MATRLIN:def 8;
then LineVec2Mx Ai = (LineVec2Mx ((b1 /. i) |-- b1)) * M by A1, A4, Th32
.= (LineVec2Mx (Line ((1. (K,(len b1))),i))) * M by A7, Th19
.= LineVec2Mx (Line (((1. (K,(len b1))) * M),i)) by A1, A6, Th35, MATRIX_0:24
.= LineVec2Mx (Line (M,i)) by A1, MATRIXR2:68 ;
then A8: Ai = Line ((LineVec2Mx (Line (M,i))),1) by MATRIX15:25
.= Line (M,i) by MATRIX15:25
.= M . i by A5, MATRIX_0:52 ;
i in dom (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) by A1, A2, A4, FINSEQ_3:25;
hence M . i = (AutMt ((Mx2Tran (M,b1,b2)),b1,b2)) . i by A8, PARTFUN1:def 6; :: thesis: verum

end;

hence AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M by A2, FINSEQ_1:14, MATRIX_0:25; :: thesis: verum