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 j being Element of NAT st j >= 1 & j < len p holds
for l being Element of NAT st l in dom (p . j) holds
(p . j) . l = (p . (j + 1)) . l
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 j being Element of NAT st j >= 1 & j < len p holds
for l being Element of NAT st l in dom (p . j) holds
(p . j) . l = (p . (j + 1)) . l
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 j being Element of NAT st j >= 1 & j < len p holds
for l being Element of NAT st l in dom (p . j) holds
(p . j) . l = (p . (j + 1)) . l )
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: for j being Element of NAT st j >= 1 & j < len p holds
for l being Element of NAT st l in dom (p . j) holds
(p . j) . l = (p . (j + 1)) . l
let j be Element of NAT ; :: thesis: ( j >= 1 & j < len p implies for l being Element of NAT st l in dom (p . j) holds
(p . j) . l = (p . (j + 1)) . l )
assume A2: ( j >= 1 & j < len p ) ; :: thesis: for l being Element of NAT st l in dom (p . j) holds
(p . j) . l = (p . (j + 1)) . l
let l be Element of NAT ; :: thesis: ( l in dom (p . j) implies (p . j) . l = (p . (j + 1)) . l )
assume A3: l in dom (p . j) ; :: thesis: (p . j) . l = (p . (j + 1)) . l
p . (j + 1) = (p . j) ^ (M . (j + 1)) by A1, A2;
hence (p . j) . l = (p . (j + 1)) . l by A3, FINSEQ_1:def 7; :: thesis: verum