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