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

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

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

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

end;

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

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 b19 by Th21;
then A6: (AutEqMt (id V1),b1,b19) * A9 = AutMt ((id V1) * (id V1)),b1,b1 by A3, A4, MATRLIN:46
.= 1. K,(len b1) by A5, Th28 ;
len b1 >= 1 by A4, NAT_1:19;
then 1_ K = Det ((AutEqMt (id V1),b1,b19) * A9) by A6, MATRIX_7:16
.= (Det (AutEqMt (id V1),b1,b19)) * (Det A9) by A4, MATRIX11:62 ;
then Det (AutEqMt (id V1),b1,b19) <> 0. K by VECTSP_1:44;
then A7: AutEqMt (id V1),b1,b19 is invertible by LAPLACE:34;
then (AutEqMt (id V1),b1,b19) ~ is_reverse_of AutEqMt (id V1),b1,b19 by MATRIX_6:def 4;
then (AutEqMt (id V1),b1,b19) * ((AutEqMt (id V1),b1,b19) ~ ) = 1. K,(len b1) by MATRIX_6:def 2;
hence ( AutEqMt (id V1),b1,b19 is invertible & AutEqMt (id V1),b19,b1 = (AutEqMt (id V1),b1,b19) ~ ) by A6, A7, MATRIX_8:19; :: thesis: verum

end;

end;