let n, i, j be Nat; :: thesis:
let M be Matrix of n + 1,F_Real; :: thesis:
assume AS: ( M is Matrix of n + 1,F_Rat & [i,j] in Indices M ) ; :: thesis:
(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

suppose 0 < n ; :: thesis:

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

end;

suppose not 0 < n ; :: thesis:

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

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: