{} is PartFunc of NAT,D by RELSET_1:25;
hence ex b₁ being PartFunc of NAT,D st b₁ is FinSequence-like ; :: thesis: verum