let n, m be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: Del M,(n + 1) is Matrix of n,m,D
A1: len M = n + 1 by MATRIX_1:def 3;
then A2: len (Del M,(n + 1)) = n by Th3;

per cases ( n = 0 or n > 0 ) ;

suppose A3: n = 0 ; :: thesis: Del M,(n + 1) is Matrix of n,m,D

then Del M,(n + 1) = {} by A2;
hence Del M,(n + 1) is Matrix of n,m,D by A3, MATRIX_1:13; :: thesis: verum

end;

suppose A4: n > 0 ; :: thesis: Del M,(n + 1) is Matrix of n,m,D

width M = m by A1, MATRIX_1:20;
then width (Del M,(n + 1)) = m by A4, Th4;
hence Del M,(n + 1) is Matrix of n,m,D by A2, A4, MATRIX_1:20; :: thesis: verum

end;

end;