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;

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

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))) )

hence
( n > 0 implies width M = width (Del (M,(n + 1))) )
; :: thesis: ( M1 = <*(M . (n + 1))*> implies width M = width M1 )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;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

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