let n, m be 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 ) )
let D be 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 M be 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 M1 be Matrix of D; ( ( 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;
then
n + 1 in Seg (len M)
by FINSEQ_1:6;
then
n + 1 in dom M
by FINSEQ_1:def 3;
then A2:
M . (n + 1) = Line M,(n + 1)
by MATRIX_2:18;
now assume A3:
n > 0
;
width M = width (Del M,(n + 1))
len (Del M,(n + 1)) = n
by A1, Th3;
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_1:def 4;
consider n1 being
Nat such that A6:
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;
consider s1 being
FinSequence such that A7:
s1 in rng M
and A8:
len s1 = width M
by A1, MATRIX_1:def 4;
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:115;
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;
verum end;
hence
( n > 0 implies width M = width (Del M,(n + 1)) )
; ( M1 = <*(M . (n + 1))*> implies width M = width M1 )
assume
M1 = <*(M . (n + 1))*>
; width M = width M1
then reconsider M2 = M1 as Matrix of 1, len (Line M,(n + 1)),D by A2, MATRIX_1:11;
thus width M =
len (Line M,(n + 1))
by MATRIX_1:def 8
.=
width M2
by MATRIX_1:24
.=
width M1
; verum