let p be FinSequence; :: thesis: for i being Nat st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
let i be Nat; :: thesis: ( i < len p implies p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> )
assume i < len p ; :: thesis: p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
then A1: i + 1 <= len p by NAT_1:13;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom p by A1, FINSEQ_3:25;
hence p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by Th10; :: thesis: verum