let n, i, j, k, m be Nat; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ; :: thesis: verum