let n be Nat; :: thesis: for K being Field

for M being Matrix of n,K st M is invertible holds

for i, j being Nat st [i,j] in Indices (M ~) holds

(M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i))

let K be Field; :: thesis: for M being Matrix of n,K st M is invertible holds

for i, j being Nat st [i,j] in Indices (M ~) holds

(M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i))

let M be Matrix of n,K; :: thesis: ( M is invertible implies for i, j being Nat st [i,j] in Indices (M ~) holds

(M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i)) )

assume M is invertible ; :: thesis: for i, j being Nat st [i,j] in Indices (M ~) holds

(M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i))

then A1: Det M <> 0. K by Th34;

set D = Det M;

set COF = Matrix_of_Cofactor M;

let i, j be Nat; :: thesis: ( [i,j] in Indices (M ~) implies (M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i)) )

assume [i,j] in Indices (M ~) ; :: thesis: (M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i))

then A2: [i,j] in Indices ((Matrix_of_Cofactor M) @) by MATRIX_0:26;

then A3: [j,i] in Indices (Matrix_of_Cofactor M) by MATRIX_0:def 6;

thus (M ~) * (i,j) = (((Det M) ") * ((Matrix_of_Cofactor M) @)) * (i,j) by A1, Th35

.= ((Det M) ") * (((Matrix_of_Cofactor M) @) * (i,j)) by A2, MATRIX_3:def 5

.= ((Det M) ") * ((Matrix_of_Cofactor M) * (j,i)) by A3, MATRIX_0:def 6

.= ((Det M) ") * (Cofactor (M,j,i)) by A3, Def6

.= (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i)) by GROUP_1:def 3 ; :: thesis: verum

for M being Matrix of n,K st M is invertible holds

for i, j being Nat st [i,j] in Indices (M ~) holds

(M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i))

let K be Field; :: thesis: for M being Matrix of n,K st M is invertible holds

for i, j being Nat st [i,j] in Indices (M ~) holds

(M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i))

let M be Matrix of n,K; :: thesis: ( M is invertible implies for i, j being Nat st [i,j] in Indices (M ~) holds

(M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i)) )

assume M is invertible ; :: thesis: for i, j being Nat st [i,j] in Indices (M ~) holds

(M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i))

then A1: Det M <> 0. K by Th34;

set D = Det M;

set COF = Matrix_of_Cofactor M;

let i, j be Nat; :: thesis: ( [i,j] in Indices (M ~) implies (M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i)) )

assume [i,j] in Indices (M ~) ; :: thesis: (M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i))

then A2: [i,j] in Indices ((Matrix_of_Cofactor M) @) by MATRIX_0:26;

then A3: [j,i] in Indices (Matrix_of_Cofactor M) by MATRIX_0:def 6;

thus (M ~) * (i,j) = (((Det M) ") * ((Matrix_of_Cofactor M) @)) * (i,j) by A1, Th35

.= ((Det M) ") * (((Matrix_of_Cofactor M) @) * (i,j)) by A2, MATRIX_3:def 5

.= ((Det M) ") * ((Matrix_of_Cofactor M) * (j,i)) by A3, MATRIX_0:def 6

.= ((Det M) ") * (Cofactor (M,j,i)) by A3, Def6

.= (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i)) by GROUP_1:def 3 ; :: thesis: verum