set q = p | (Seg m);
len p = m + 1 by CARD_1:def 13;
then p = (p | (Seg m)) ^ <*(p . (m + 1))*> by FINSEQ_3:61;
hence for b₁ being set st b₁ = ((p | (Seg m)) ^ <*(p . (m + 1))*>) \+\ p holds
b₁ is empty ; :: thesis: verum