let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
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 K; :: 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: len b1 = dim V1 by Th21
.= len b1' by Th21 ;
reconsider A' = AutEqMt (id V1),b1',b1 as Matrix of len b1, len b1,K by A1;
A2: ( AutEqMt (id V1),b1,b1' = AutMt (id V1),b1,b1' & A' = AutMt (id V1),b1',b1 ) by A1, Def2;
A3: 1_ K <> 0. K ;

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 A3, 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') ~ )

then A5: len b1 >= 1 by NAT_1:19;
dom (id V1) = the carrier of V1 by RELAT_1:71;
then A6: (id V1) * (id V1) = id V1 by RELAT_1:78;
len b1 = dim V1 by Th21;
then ( id V1 is linear & len b1 = len b1' ) by Th21, MOD_2:13;
then A7: (AutEqMt (id V1),b1,b1') * A' = AutMt ((id V1) * (id V1)),b1,b1 by A4, A2, MATRLIN:46
.= 1. K,(len b1) by Th28, A6 ;
then 1_ K = Det ((AutEqMt (id V1),b1,b1') * A') by A5, 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 A8: 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 A7, A8, MATRIX_8:19; :: thesis: verum

end;

end;