let n, i, j, k, m be Nat; for M being Matrix of n + 1,F_Real st 0 < n & M is Matrix of n + 1,F_Rat & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) holds
(Delete (M,i,j)) * (k,m) is Element of F_Rat
let M be Matrix of n + 1,F_Real; ( 0 < n & M is Matrix of n + 1,F_Rat & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) implies (Delete (M,i,j)) * (k,m) is Element of F_Rat )
assume that
A1:
0 < n
and
A2:
M is Matrix of n + 1,F_Rat
and
A3:
[i,j] in Indices M
and
A4:
[k,m] in Indices (Delete (M,i,j))
; (Delete (M,i,j)) * (k,m) is Element of F_Rat
reconsider L = M as Matrix of n + 1,F_Rat by A2;
(Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)
by LmSign1F, A1, A3, A4;
hence
(Delete (M,i,j)) * (k,m) is Element of F_Rat
; verum