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