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