reconsider i = i as Element of NAT by ORDINAL1:def 12;
f +* (i,p) is FinSequence of D ;
hence ( Replace (f,i,p) is FinSequence of D & ( for b₁ being FinSequence of D holds verum ) ) ; :: thesis: verum