theorem LmSign1E: :: ZMODLAT2:52

for n, i, j 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 holds
Delete (M,i,j) = Delete (L,i,j)