theorem :: ZMODLAT2:56

for n, i, j being 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