let p, P be set ; :: thesis: ( p in P implies p multitude_of = 0 )
assume A1: p in P ; :: thesis: p multitude_of = 0
then reconsider P = P as non empty set ;
p in dom ({$} P) by A1, FUNCT_2:def 1;
then ({$} P) . p in rng ({$} P) by FUNCT_1:def 5;
then ({$} P) . p in {0 } by FUNCOP_1:14;
hence p multitude_of = 0 by TARSKI:def 1; :: thesis: verum