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