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
( len (p . 1) = width M & ( for j being Nat st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,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
( len (p . 1) = width M & ( for j being Nat st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,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 ( len (p . 1) = width M & ( for j being Nat st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,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))
; ( len (p . 1) = width M & ( for j being Nat st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) ) )
per cases
( len M = 0 or len M > 0 )
;
suppose A4:
len M = 0
;
( len (p . 1) = width M & ( for j being Nat st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) ) )then
p = {}
by A1;
then
p . 1
= {}
by FUNCT_1:def 2, RELAT_1:38;
hence
len (p . 1) = width M
by A4, MATRIX_0:def 3;
for j being Nat st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,j) )let j be
Nat;
( [1,j] in Indices M implies ( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) )A5:
Seg (len M) = {}
by A4;
assume
[1,j] in Indices M
;
( j in dom (p . 1) & (p . 1) . j = M * (1,j) )hence
(
j in dom (p . 1) &
(p . 1) . j = M * (1,
j) )
by A5, MATRPROB:12;
verum end; suppose
len M > 0
;
( len (p . 1) = width M & ( for j being Nat st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) ) )then
1
<= len p
by A1, NAT_1:14;
then
1
in Seg (len p)
by FINSEQ_1:1;
then
1
in dom p
by FINSEQ_1:def 3;
hence A6:
len (p . 1) =
1
* (width M)
by A1, A2, A3, Th29
.=
width M
;
for j being Nat st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,j) )let j be
Nat;
( [1,j] in Indices M implies ( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) )assume A7:
[1,j] in Indices M
;
( j in dom (p . 1) & (p . 1) . j = M * (1,j) )
j in Seg (width M)
by A7, MATRPROB:12;
hence
(
j in dom (p . 1) &
(p . 1) . j = M * (1,
j) )
by A2, A6, A7, FINSEQ_1:def 3, MATRPROB:14;
verum end;