let D be non empty set ; for M being Matrix of D
for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being Nat st i in dom p & j in dom p & i <= j holds
dom (p . i) c= dom (p . j)
let M be Matrix of D; for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being Nat st i in dom p & j in dom p & i <= j holds
dom (p . i) c= dom (p . j)
let p be FinSequence of D * ; ( len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) implies for i, j being Nat st i in dom p & j in dom p & i <= j holds
dom (p . i) c= dom (p . j) )
assume that
A1:
len p = len M
and
A2:
p . 1 = M . 1
and
A3:
for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1))
; for i, j being Nat st i in dom p & j in dom p & i <= j holds
dom (p . i) c= dom (p . j)
let i, j be Nat; ( i in dom p & j in dom p & i <= j implies dom (p . i) c= dom (p . j) )
assume that
A4:
i in dom p
and
A5:
j in dom p
and
A6:
i <= j
; dom (p . i) c= dom (p . j)
A7:
len (p . j) = j * (width M)
by A1, A2, A3, A5, Th29;
len (p . i) = i * (width M)
by A1, A2, A3, A4, Th29;
then
len (p . i) <= len (p . j)
by A6, A7, NAT_1:4;
then
Seg (len (p . i)) c= Seg (len (p . j))
by FINSEQ_1:5;
then
dom (p . i) c= Seg (len (p . j))
by FINSEQ_1:def 3;
hence
dom (p . i) c= dom (p . j)
by FINSEQ_1:def 3; verum