let K be Field; :: thesis: for i, j, n being Nat

for M being Matrix of n,K st i in dom M holds

len (Deleting (M,i,j)) = n -' 1

let i, j, n be Nat; :: thesis: for M being Matrix of n,K st i in dom M holds

len (Deleting (M,i,j)) = n -' 1

let M be Matrix of n,K; :: thesis: ( i in dom M implies len (Deleting (M,i,j)) = n -' 1 )

assume A1: i in dom M ; :: thesis: len (Deleting (M,i,j)) = n -' 1

A2: len M = n by MATRIX_0:def 2;

thus len (Deleting (M,i,j)) = len (DelLine (M,i)) by MATRIX_0:def 13

.= n -' 1 by A1, A2, Th1 ; :: thesis: verum

for M being Matrix of n,K st i in dom M holds

len (Deleting (M,i,j)) = n -' 1

let i, j, n be Nat; :: thesis: for M being Matrix of n,K st i in dom M holds

len (Deleting (M,i,j)) = n -' 1

let M be Matrix of n,K; :: thesis: ( i in dom M implies len (Deleting (M,i,j)) = n -' 1 )

assume A1: i in dom M ; :: thesis: len (Deleting (M,i,j)) = n -' 1

A2: len M = n by MATRIX_0:def 2;

thus len (Deleting (M,i,j)) = len (DelLine (M,i)) by MATRIX_0:def 13

.= n -' 1 by A1, A2, Th1 ; :: thesis: verum