let m, n 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_0:def 2;
then A2: len (Del (M,(n + 1))) = n by Th1;

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_0: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_0:20;
then width (Del (M,(n + 1))) = m by A4, Th2;
hence Del (M,(n + 1)) is Matrix of n,m,D by A2, A4, MATRIX_0:20; :: thesis: verum

end;

end;