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

(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