theorem Th2: :: MATRLIN:2

for m, n being Nat
for D being non empty set
for M being Matrix of n + 1,m,D
for M1 being Matrix of D holds
( ( n > 0 implies width M = width (Del (M,(n + 1))) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) )