( {} is finite & {} is PartFunc of A,B ) by RELSET_1:25;
hence ex b₁ being PartFunc of A,B st b₁ is finite ; :: thesis: verum