consider m being Nat such that
A1: len p = m + 1 by NAT_1:6;
reconsider pp = p as U -valued 1 + m -element FinSequence by A1, CARD_1:def 7;
{(pp . 1)} \ U = {} ;
hence for b₁ being set st b₁ = {(p . 1)} \ U holds
b₁ is empty ; :: thesis: verum