let k be Nat; :: thesis: for D being set
for f being FinSequence of D st k + 1 <= len f holds
f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*>
let D be set ; :: thesis: for f being FinSequence of D st k + 1 <= len f holds
f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*>
let f be FinSequence of D; :: thesis: ( k + 1 <= len f implies f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> )
A1: 1 <= k + 1 by NAT_1:12;
assume k + 1 <= len f ; :: thesis: f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*>
then A2: k + 1 in dom f by A1, FINSEQ_3:25;
then f | (Seg (k + 1)) = (f | k) ^ <*(f . (k + 1))*> by Th10
.= (f | k) ^ <*(f /. (k + 1))*> by A2, PARTFUN1:def 6 ;
hence f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*> ; :: thesis: verum