let K be Field; :: thesis: for V1 being finite-dimensional VectSp of finite-dimensional
for b1, b1' being OrdBasis of V1 holds
( AutEqMt (id V1),b1,b1' is invertible & AutEqMt (id V1),b1',b1 = (AutEqMt (id V1),b1,b1') ~ )
let V1 be finite-dimensional VectSp of finite-dimensional ; :: thesis: for b1, b1' being OrdBasis of V1 holds
( AutEqMt (id V1),b1,b1' is invertible & AutEqMt (id V1),b1',b1 = (AutEqMt (id V1),b1,b1') ~ )
let b1, b1' be OrdBasis of V1; :: thesis: ( AutEqMt (id V1),b1,b1' is invertible & AutEqMt (id V1),b1',b1 = (AutEqMt (id V1),b1,b1') ~ )
set A = AutEqMt (id V1),b1,b1';
A1: 1_ K <> 0. K ;
A2: len b1 = dim V1 by Th21
.= len b1' by Th21 ;
then reconsider A' = AutEqMt (id V1),b1',b1 as Matrix of the carrier of K, len b1, ;
A3: ( AutEqMt (id V1),b1,b1' = AutMt (id V1),b1,b1' & A' = AutMt (id V1),b1',b1 ) by A2, Def2;

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

suppose len b1 = 0 ; :: thesis: ( AutEqMt (id V1),b1,b1' is invertible & AutEqMt (id V1),b1',b1 = (AutEqMt (id V1),b1,b1') ~ )

then ( Det (AutEqMt (id V1),b1,b1') = 1_ K & A' = (AutEqMt (id V1),b1,b1') ~ ) by MATRIXR2:41, MATRIX_1:36;
hence ( AutEqMt (id V1),b1,b1' is invertible & AutEqMt (id V1),b1',b1 = (AutEqMt (id V1),b1,b1') ~ ) by A1, LAPLACE:34; :: thesis: verum

end;

suppose A4: (len b1) + 0 > 0 ; :: thesis: ( AutEqMt (id V1),b1,b1' is invertible & AutEqMt (id V1),b1',b1 = (AutEqMt (id V1),b1,b1') ~ )

dom (id V1) = the carrier of V1 by RELAT_1:71;
then A5: (id V1) * (id V1) = id V1 by RELAT_1:78;
len b1 = dim V1 by Th21;
then len b1 = len b1' by Th21;
then A6: (AutEqMt (id V1),b1,b1') * A' = AutMt ((id V1) * (id V1)),b1,b1 by A3, A4, MATRLIN:46, MOD_2:13
.= 1. K,(len b1) by A5, Th28 ;
len b1 >= 1 by A4, NAT_1:19;
then 1_ K = Det ((AutEqMt (id V1),b1,b1') * A') by A6, MATRIX_7:16
.= (Det (AutEqMt (id V1),b1,b1')) * (Det A') by A4, MATRIX11:62 ;
then Det (AutEqMt (id V1),b1,b1') <> 0. K by VECTSP_1:44;
then A7: AutEqMt (id V1),b1,b1' is invertible by LAPLACE:34;
then (AutEqMt (id V1),b1,b1') ~ is_reverse_of AutEqMt (id V1),b1,b1' by MATRIX_6:def 4;
then (AutEqMt (id V1),b1,b1') * ((AutEqMt (id V1),b1,b1') ~ ) = 1. K,(len b1) by MATRIX_6:def 2;
hence ( AutEqMt (id V1),b1,b1' is invertible & AutEqMt (id V1),b1',b1 = (AutEqMt (id V1),b1,b1') ~ ) by A6, A7, MATRIX_8:19; :: thesis: verum

end;

end;