let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
(((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n
let K be Field; :: thesis: for M being Matrix of n,K st Det M <> 0. K holds
(((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n
let M be Matrix of n,K; :: thesis: ( Det M <> 0. K implies (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n )
set D = Det M;
set D9 = (Det M) " ;
set C = Matrix_of_Cofactor M;
set DC = ((Det M) " ) * ((Matrix_of_Cofactor M) @ );
set CM = (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M;
set ID = 1. K,n;
assume A1: Det M <> 0. K ; :: thesis: (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n

now

A2: Indices ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) = Indices (1. K,n) by MATRIX_1:27;
reconsider N = n as Element of NAT by ORDINAL1:def 13;
let i, j be Nat; :: thesis: ( [i,j] in Indices ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) implies (1. K,n) * b₁,b₂ = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * b₁,b₂ )
assume A3: [i,j] in Indices ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) ; :: thesis: (1. K,n) * b₁,b₂ = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * b₁,b₂
reconsider COL = Col M,j, L = Line ((Matrix_of_Cofactor M) @ ),i as Element of N -tuples_on the carrier of K by MATRIX_1:25;
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 13;
A4: len M = n by MATRIX_1:25;
A5: Indices ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A6: i in Seg n by A3, ZFMISC_1:106;
then A7: 1 <= i by FINSEQ_1:3;
A8: j in Seg n by A3, A5, ZFMISC_1:106;
len ((Matrix_of_Cofactor M) @ ) = n by MATRIX_1:25;
then i <= len ((Matrix_of_Cofactor M) @ ) by A6, FINSEQ_1:3;
then Line (((Det M) " ) * ((Matrix_of_Cofactor M) @ )),i = ((Det M) " ) * L by A7, MATRIXR1:20;
then mlt (Line (((Det M) " ) * ((Matrix_of_Cofactor M) @ )),i),(Col M,j) = ((Det M) " ) * (mlt L,COL) by FVSUM_1:83;
then A9: (Line (((Det M) " ) * ((Matrix_of_Cofactor M) @ )),i) "*" (Col M,j) = ((Det M) " ) * ((Line ((Matrix_of_Cofactor M) @ ),i) "*" (Col M,j)) by FVSUM_1:92
.= ((Det M) " ) * (Det (RLine (M @ ),i9,(Line (M @ ),j9))) by A6, A8, Th32 ;
A10: width (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) = n by MATRIX_1:25;
then A11: ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * i,j = ((Det M) " ) * (Det (RLine (M @ ),i,(Line (M @ ),j))) by A3, A4, A9, MATRIX_3:def 4;

per cases ( i = j or i <> j ) ;

suppose A12: i = j ; :: thesis: (1. K,n) * b₁,b₂ = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * b₁,b₂

then A13: RLine (M @ ),i,(Line (M @ ),j) = M @ by MATRIX11:30;
A14: Det M = Det (M @ ) by MATRIXR2:43;
A15: ((Det M) " ) * (Det M) = 1_ K by A1, VECTSP_1:def 22;
(1. K,n) * i,j = 1_ K by A3, A2, A12, MATRIX_1:def 12;
hence (1. K,n) * i,j = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * i,j by A3, A10, A4, A9, A13, A15, A14, MATRIX_3:def 4; :: thesis: verum

end;

suppose A16: i <> j ; :: thesis: (1. K,n) * b₁,b₂ = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * b₁,b₂

then A17: (1. K,n) * i,j = 0. K by A3, A2, MATRIX_1:def 12;
Det (RLine (M @ ),i9,(Line (M @ ),j9)) = 0. K by A6, A8, A16, MATRIX11:51;
hence (1. K,n) * i,j = ((((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M) * i,j by A11, A17, VECTSP_1:36; :: thesis: verum

end;

end;

end;

hence (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n by MATRIX_1:28; :: thesis: verum