let n, i, j 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 holds
Delete (M,i,j) is Matrix of n,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 implies Delete (M,i,j) is Matrix of n,F_Rat )
assume that
A1: 0 < n and
A2: M is Matrix of n + 1,F_Rat and
A3: [i,j] in Indices M ; :: thesis: Delete (M,i,j) is Matrix of n,F_Rat
reconsider L = M as Matrix of n + 1,F_Rat by A2;
X1: Delete (M,i,j) = Delete (L,i,j) by LmSign1E, A1, A3;
(n + 1) -' 1 = n by NAT_D:34;
hence Delete (M,i,j) is Matrix of n,F_Rat by X1; :: thesis: verum