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 & len (AutMt (Mx2Tran M,b1,b2),b1,b2) = len b1 & len (1. K,(len b1)) = len b1 & width (1. K,(len b1)) = len b1 ) by MATRIX_1:25, MATRIX_1:26;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len M implies M . i = (AutMt (Mx2Tran M,b1,b2),b1,b2) . i )
assume A2: ( 1 <= i & i <= len M ) ; :: thesis: M . i = (AutMt (Mx2Tran M,b1,b2),b1,b2) . i
A3: ( i in dom b1 & i in dom (AutMt (Mx2Tran M,b1,b2),b1,b2) & i in dom (1. K,(len b1)) & i in Seg (len b1) ) by A1, A2, FINSEQ_1:3, FINSEQ_3:27;
then (AutMt (Mx2Tran M,b1,b2),b1,b2) /. i = ((Mx2Tran M,b1,b2) . (b1 /. i)) |-- b2 by MATRLIN:def 10;
then LineVec2Mx ((AutMt (Mx2Tran M,b1,b2),b1,b2) /. i) = (LineVec2Mx ((b1 /. i) |-- b1)) * M by A1, A2, Th32
.= (LineVec2Mx (Line (1. K,(len b1)),i)) * M by A3, Th19
.= LineVec2Mx (Line ((1. K,(len b1)) * M),i) by A1, A3, Th35
.= LineVec2Mx (Line M,i) by A1, MATRIXR2:68 ;
then (AutMt (Mx2Tran M,b1,b2),b1,b2) /. i = Line (LineVec2Mx (Line M,i)),1 by MATRIX15:25
.= Line M,i by MATRIX15:25
.= M . i by A3, MATRIX_2:10 ;
hence M . i = (AutMt (Mx2Tran M,b1,b2),b1,b2) . i by A3, PARTFUN1:def 8; :: thesis: verum

end;

hence AutMt (Mx2Tran M,b1,b2),b1,b2 = M by A1, FINSEQ_1:18; :: thesis: verum