theorem LmSign1F: :: ZMODLAT2:50
for n, i, j, k, m being Nat
for M being Matrix of n + 1,F_Real
for L being Matrix of n + 1,F_Rat st 0 < n & M = L & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) holds
(Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)