let D be set ; :: thesis: for p being FinSequence of D
for i being Nat st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>
let p be FinSequence of D; :: 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 A2: i + 1 in dom p by A1, FINSEQ_3:25;
p | (i + 1) = (p | i) ^ <*(p /. (i + 1))*> by A1, Th85;
hence p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by A2, PARTFUN1:def 6; :: thesis: verum