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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for k being Nat st k in dom p holds
len (p . k) = k * (width M)
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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for k being Nat st k in dom p holds
len (p . k) = k * (width M)
let p be FinSequence of D * ; :: thesis: ( 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 k being Nat st k in dom p holds
len (p . k) = k * (width M) )
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)) ; :: thesis: for k being Nat st k in dom p holds
len (p . k) = k * (width M)
defpred S₁[ Nat] means ( $1 >= 1 & $1 <= len M implies len (p . $1) = $1 * (width M) );
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: ( n >= 1 & n <= len M implies len (p . n) = n * (width M) ) ; :: thesis: S₁[n + 1]
assume that
A6: n + 1 >= 1 and
A7: n + 1 <= len M ; :: thesis: len (p . (n + 1)) = (n + 1) * (width M)

now :: thesis: len (p . (n + 1)) = (n + 1) * (width M)

per cases ( n = 0 or n <> 0 ) ;

suppose A8: n = 0 ; :: thesis: len (p . (n + 1)) = (n + 1) * (width M)

then 1 in dom M by A7, FINSEQ_3:25;
hence len (p . (n + 1)) = (n + 1) * (width M) by A2, A8, MATRIX_0:36; :: thesis: verum

end;

suppose A9: n <> 0 ; :: thesis: len (p . (n + 1)) = (n + 1) * (width M)

A10: n + 1 in dom M by A6, A7, FINSEQ_3:25;
n < len M by A7, NAT_1:13;
then p . (n + 1) = (p . n) ^ (M . (n + 1)) by A3, A9, NAT_1:14;
then len (p . (n + 1)) = (len (p . n)) + (len (M . (n + 1))) by FINSEQ_1:22
.= (n * (width M)) + (width M) by A5, A7, A9, A10, MATRIX_0:36, NAT_1:13, NAT_1:14
.= (n + 1) * (width M) ;
hence len (p . (n + 1)) = (n + 1) * (width M) ; :: thesis: verum

end;

end;

end;

hence len (p . (n + 1)) = (n + 1) * (width M) ; :: thesis: verum

end;

A11: S₁[ 0 ] ;
A12: for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A4);
let k be Nat; :: thesis: ( k in dom p implies len (p . k) = k * (width M) )
assume k in dom p ; :: thesis: len (p . k) = k * (width M)
then A13: k in Seg (len p) by FINSEQ_1:def 3;
then A14: k <= len p by FINSEQ_1:1;
k >= 1 by A13, FINSEQ_1:1;
hence len (p . k) = k * (width M) by A1, A12, A14; :: thesis: verum