let n, i, j be Nat; 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; ( 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 )
; 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; verum