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_1:def 3;
thus len (Deleting M,i,j) = len (DelLine M,i) by MATRIX_2:def 6
.= n -' 1 by A1, A2, Th1 ; :: thesis: verum