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