consider m being Nat such that
A1: m1 = m + 1 by NAT_1:6;
set IT = {(p . m1)} \ U;
set M = m1 + n;
p in (m1 + n) -tuples_on U by Th16;
then p is Element of Funcs ((Seg (m1 + n)),U) by Lm7;
then reconsider f = p as Function of (Seg (m1 + n)),U ;
( 1 <= m + 1 & m + 1 <= (m + 1) + n ) by NAT_1:11;
then reconsider ms = m1 as Element of Seg (m1 + n) by A1, FINSEQ_1:1;
f . ms in U ;
hence for b₁ being set st b₁ = {(p . m1)} \ U holds
b₁ is empty by ZFMISC_1:60; :: thesis: verum