let D be non empty set ; :: thesis: for M being Matrix of D
for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of 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 Element of 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; :: thesis: for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of 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 Element of 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 * ; :: thesis: ( len p = len M & p . 1 = M . 1 & ( for k being Element of 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 Element of NAT st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * 1,j ) ) ) )
assume A1: ( len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ; :: thesis: ( len (p . 1) = width M & ( for j being Element of 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 A2: len M = 0 ; :: thesis: ( len (p . 1) = width M & ( for j being Element of 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 4, RELAT_1:60;
hence len (p . 1) = width M by A2, MATRIX_1:def 4; :: thesis: for j being Element of NAT st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * 1,j )
let j be Element of NAT ; :: thesis: ( [1,j] in Indices M implies ( j in dom (p . 1) & (p . 1) . j = M * 1,j ) )
assume A3: [1,j] in Indices M ; :: thesis: ( j in dom (p . 1) & (p . 1) . j = M * 1,j )
thus ( j in dom (p . 1) & (p . 1) . j = M * 1,j ) by A2, A3, FINSEQ_1:4, MATRPROB:12; :: thesis: verum

end;

suppose len M > 0 ; :: thesis: ( len (p . 1) = width M & ( for j being Element of 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:3;
then 1 in dom p by FINSEQ_1:def 3;
hence A4: len (p . 1) = 1 * (width M) by A1, Th29
.= width M ;
:: thesis: for j being Element of NAT st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * 1,j )
let j be Element of NAT ; :: thesis: ( [1,j] in Indices M implies ( j in dom (p . 1) & (p . 1) . j = M * 1,j ) )
assume A5: [1,j] in Indices M ; :: thesis: ( j in dom (p . 1) & (p . 1) . j = M * 1,j )
j in Seg (width M) by A5, MATRPROB:12;
hence ( j in dom (p . 1) & (p . 1) . j = M * 1,j ) by A1, A4, A5, FINSEQ_1:def 3, MATRPROB:14; :: thesis: verum

end;

end;