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) @)

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) @)

let M be Matrix of n,K; :: thesis: ( Det M <> 0. K implies M ~ = ((Det M) ") * ((Matrix_of_Cofactor M) @) )

set C = ((Det M) ") * ((Matrix_of_Cofactor M) @);

assume A1: Det M <> 0. K ; :: thesis: M ~ = ((Det M) ") * ((Matrix_of_Cofactor M) @)

then A2: M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n) by Th30;

(((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n) by A1, Th33;

then A3: M is_reverse_of ((Det M) ") * ((Matrix_of_Cofactor M) @) by A2, MATRIX_6:def 2;

M is invertible by A1, Th34;

hence M ~ = ((Det M) ") * ((Matrix_of_Cofactor M) @) by A3, MATRIX_6:def 4; :: thesis: verum

for M being Matrix of n,K st Det M <> 0. K holds

M ~ = ((Det M) ") * ((Matrix_of_Cofactor M) @)

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) @)

let M be Matrix of n,K; :: thesis: ( Det M <> 0. K implies M ~ = ((Det M) ") * ((Matrix_of_Cofactor M) @) )

set C = ((Det M) ") * ((Matrix_of_Cofactor M) @);

assume A1: Det M <> 0. K ; :: thesis: M ~ = ((Det M) ") * ((Matrix_of_Cofactor M) @)

then A2: M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n) by Th30;

(((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n) by A1, Th33;

then A3: M is_reverse_of ((Det M) ") * ((Matrix_of_Cofactor M) @) by A2, MATRIX_6:def 2;

M is invertible by A1, Th34;

hence M ~ = ((Det M) ") * ((Matrix_of_Cofactor M) @) by A3, MATRIX_6:def 4; :: thesis: verum