let n, m 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_1:def 3;
now assume A2:
n > 0
;
:: thesis: width M = width (Del M,(n + 1))
len (Del M,(n + 1)) = n
by A1, Th3;
then consider s being
FinSequence such that A3:
(
s in rng (Del M,(n + 1)) &
len s = width (Del M,(n + 1)) )
by A2, MATRIX_1:def 4;
consider s1 being
FinSequence such that A4:
(
s1 in rng M &
len s1 = width M )
by A1, MATRIX_1:def 4;
consider n1 being
Nat such that A5:
for
x being
set st
x in rng M holds
ex
p being
FinSequence of
D st
(
x = p &
len p = n1 )
by MATRIX_1:9;
rng (Del M,(n + 1)) c= rng M
by FINSEQ_3:115;
then consider p1 being
FinSequence of
D such that A6:
(
s = p1 &
len p1 = n1 )
by A3, A5;
consider p2 being
FinSequence of
D such that A7:
(
s1 = p2 &
len p2 = n1 )
by A4, A5;
thus
width M = width (Del M,(n + 1))
by A3, A4, A6, A7;
:: 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 A8:
M1 = <*(M . (n + 1))*>
; :: thesis: width M = width M1
n + 1 in Seg (len M)
by A1, FINSEQ_1:6;
then
n + 1 in dom M
by FINSEQ_1:def 3;
then
M . (n + 1) = Line M,(n + 1)
by MATRIX_2:18;
then reconsider M2 = M1 as Matrix of 1, len (Line M,(n + 1)),D by A8, MATRIX_1:11;
thus width M =
len (Line M,(n + 1))
by MATRIX_1:def 8
.=
width M2
by MATRIX_1:24
.=
width M1
; :: thesis: verum