let m, n be Nat; :: thesis: 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 ) )
let D be non empty set ; :: thesis: 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 ) )
let M be Matrix of n + 1,m,D; :: thesis: 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 ) )
let M1 be Matrix of D; :: thesis: ( ( n > 0 implies width M = width (Del (M,(n + 1))) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) )
A1: len M = n + 1 by MATRIX_0:def 2;
then n + 1 in Seg (len M) by FINSEQ_1:4;
then n + 1 in dom M by FINSEQ_1:def 3;
then A2: M . (n + 1) = Line (M,(n + 1)) by MATRIX_0:60;

now :: thesis: ( n > 0 implies width M = width (Del (M,(n + 1))) )

assume A3: n > 0 ; :: thesis: width M = width (Del (M,(n + 1)))
len (Del (M,(n + 1))) = n by A1, Th1;
then consider s being FinSequence such that
A4: s in rng (Del (M,(n + 1))) and
A5: len s = width (Del (M,(n + 1))) by A3, MATRIX_0:def 3;
consider n1 being Nat such that
A6: for x being object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n1 ) by MATRIX_0:9;
consider s1 being FinSequence such that
A7: s1 in rng M and
A8: len s1 = width M by A1, MATRIX_0:def 3;
A9: ex p2 being FinSequence of D st
( s1 = p2 & len p2 = n1 ) by A7, A6;
rng (Del (M,(n + 1))) c= rng M by FINSEQ_3:106;
then ex p1 being FinSequence of D st
( s = p1 & len p1 = n1 ) by A4, A6;
hence width M = width (Del (M,(n + 1))) by A5, A8, A9; :: thesis: verum

end;

hence ( n > 0 implies width M = width (Del (M,(n + 1))) ) ; :: thesis: ( M1 = <*(M . (n + 1))*> implies width M = width M1 )
assume M1 = <*(M . (n + 1))*> ; :: thesis: width M = width M1
then reconsider M2 = M1 as Matrix of 1, len (Line (M,(n + 1))),D by A2, MATRIX_0:11;
thus width M = len (Line (M,(n + 1))) by MATRIX_0:def 7
.= width M2 by MATRIX_0:23
.= width M1 ; :: thesis: verum