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