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

proof

per cases ( 0 < n or not 0 < n ) ;

suppose 0 < n ; :: thesis: Det DD in F_Rat

then DD is Matrix of n,F_Rat by LmSign1EX, AS;
hence Det DD in F_Rat by LmGM11; :: thesis: verum

end;

suppose not 0 < n ; :: thesis: Det DD in F_Rat

then n = 0 ;
then Det DD = 1. F_Real by MATRIXR2:41
.= 1 ;
hence Det DD in F_Rat ; :: thesis: verum

end;

end;

end;

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