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

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