let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) = 1. K,n
let K be Field; :: thesis: for M being Matrix of n,K st Det M <> 0. K holds
M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) = 1. K,n
let M be Matrix of n,K; :: thesis: ( Det M <> 0. K implies M * (((Det M) " ) * ((Matrix_of_Cofactor 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 MC = M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ ));
set ID = 1. K,n;
assume A1: Det M <> 0. K ; :: thesis: M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) = 1. K,n

now

A2: Indices (M * (((Det M) " ) * ((Matrix_of_Cofactor 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 (M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ ))) implies (1. K,n) * b₁,b₂ = (M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ ))) * b₁,b₂ )
assume A3: [i,j] in Indices (M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ ))) ; :: thesis: (1. K,n) * b₁,b₂ = (M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ ))) * b₁,b₂
reconsider COL = Col ((Matrix_of_Cofactor M) @ ),j, L = Line 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 (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) = n by MATRIX_1:25;
A5: Indices (M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ ))) = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A6: i in Seg n by A3, ZFMISC_1:106;
A7: j in Seg n by A3, A5, ZFMISC_1:106;
then A8: 1 <= j by FINSEQ_1:3;
width ((Matrix_of_Cofactor M) @ ) = n by MATRIX_1:25;
then j <= width ((Matrix_of_Cofactor M) @ ) by A7, FINSEQ_1:3;
then Col (((Det M) " ) * ((Matrix_of_Cofactor M) @ )),j = ((Det M) " ) * COL by A8, MATRIXR1:19;
then mlt (Line M,i),(Col (((Det M) " ) * ((Matrix_of_Cofactor M) @ )),j) = ((Det M) " ) * (mlt L,COL) by FVSUM_1:83;
then A9: (Line M,i) "*" (Col (((Det M) " ) * ((Matrix_of_Cofactor M) @ )),j) = ((Det M) " ) * ((Line M,i) "*" (Col ((Matrix_of_Cofactor M) @ ),j)) by FVSUM_1:92
.= ((Det M) " ) * (Det (RLine M,j9,(Line M,i9))) by A7, Th29 ;
A10: width M = n by MATRIX_1:25;
then A11: (M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ ))) * i,j = ((Det M) " ) * (Det (RLine M,j,(Line M,i))) 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₂ = (M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ ))) * b₁,b₂

then A13: RLine M,j,(Line M,i) = M by MATRIX11:30;
A14: (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 = (M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ ))) * i,j by A3, A10, A4, A9, A13, A14, MATRIX_3:def 4; :: thesis: verum

end;

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

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

end;

end;

end;

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