let m, n 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_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 ( n > 0 implies width M = width (Del (M,(n + 1))) )assume A3:
n > 0
;
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;
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_0:11;
thus width M =
len (Line (M,(n + 1)))
by MATRIX_0:def 7
.=
width M2
by MATRIX_0:23
.=
width M1
; verum