(<*x*> ^ p) . 1 = x by FINSEQ_1:41;
hence for b₁ being set st b₁ = ((<*x*> ^ p) . 1) \+\ x holds
b₁ is empty ; :: thesis: verum