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;

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;