set p = n |-> {{}};
take n |-> {{}} ; :: thesis: n |-> {{}} is non-empty
not {} in rng (n |-> {{}})
proof
assume {} in rng (n |-> {{}}) ; :: thesis: contradiction
then consider a being object such that
A1: a in dom (n |-> {{}}) and
A2: {} = (n |-> {{}}) . a by FUNCT_1:def 3;
a in Seg n by FINSEQ_1:89, A1;
hence contradiction by A2, FINSEQ_2:57; :: thesis: verum
end;
hence n |-> {{}} is non-empty by RELAT_1:def 9; :: thesis: verum