let n, i, j be Nat; :: thesis: for M being Matrix of n + 1,F_Real st M is Matrix of n + 1,F_Rat & [i,j] in Indices M holds

Cofactor (M,i,j) in F_Rat

let M be Matrix of n + 1,F_Real; :: thesis: ( M is Matrix of n + 1,F_Rat & [i,j] in Indices M implies Cofactor (M,i,j) in F_Rat )

assume AS: ( M is Matrix of n + 1,F_Rat & [i,j] in Indices M ) ; :: thesis: Cofactor (M,i,j) in F_Rat

(n + 1) -' 1 = n by NAT_D:34;

then reconsider DD = Delete (M,i,j) as Matrix of n,F_Real ;

Det DD in F_Rat then A1: Minor (M,i,j) in F_Rat by NAT_D:34;

(power F_Real) . ((- (1_ F_Real)),(i + j)) in F_Rat by LmSign1D;

hence Cofactor (M,i,j) in F_Rat by A1, RAT_1:def 2; :: thesis: verum

Cofactor (M,i,j) in F_Rat

let M be Matrix of n + 1,F_Real; :: thesis: ( M is Matrix of n + 1,F_Rat & [i,j] in Indices M implies Cofactor (M,i,j) in F_Rat )

assume AS: ( M is Matrix of n + 1,F_Rat & [i,j] in Indices M ) ; :: thesis: Cofactor (M,i,j) in F_Rat

(n + 1) -' 1 = n by NAT_D:34;

then reconsider DD = Delete (M,i,j) as Matrix of n,F_Real ;

Det DD in F_Rat then A1: Minor (M,i,j) in F_Rat by NAT_D:34;

(power F_Real) . ((- (1_ F_Real)),(i + j)) in F_Rat by LmSign1D;

hence Cofactor (M,i,j) in F_Rat by A1, RAT_1:def 2; :: thesis: verum