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

proof

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

now

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:27;
hence len (p . (n + 1)) = (n + 1) * (width M) by A2, A8, GOBRD13:4; :: thesis: verum

end;

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

A10: n + 1 in dom M by A7, FINSEQ_3:27;
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:35
.= (n * (width M)) + (width M) by A6, A7, A9, A10, GOBRD13:4, 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: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A5);
let k be Element of NAT ; :: thesis: ( k in dom p implies len (p . k) = k * (width M) )
assume A12: k in dom p ; :: thesis: len (p . k) = k * (width M)
k in Seg (len p) by A12, FINSEQ_1:def 3;
then ( k >= 1 & k <= len p ) by FINSEQ_1:3;
hence len (p . k) = k * (width M) by A1, A11; :: thesis: verum