let m, n be Nat; for D being non empty set
for M being Matrix of n + 1,m,D holds Del (M,(n + 1)) is Matrix of n,m,D
let D be non empty set ; for M being Matrix of n + 1,m,D holds Del (M,(n + 1)) is Matrix of n,m,D
let M be Matrix of n + 1,m,D; Del (M,(n + 1)) is Matrix of n,m,D
A1:
len M = n + 1
by MATRIX_0:def 2;
then A2:
len (Del (M,(n + 1))) = n
by Th1;