deffunc H₄( Element of A) -> Element of NAT = card (dom ({$1} | p));
consider m being Function of A,NAT such that
A1: for a being Element of A holds m . a = H₄(a) from FUNCT_2:sch 4();
m is Multiset of A by Th28;
hence ex b₁ being Multiset of A st
for a being Element of A holds b₁ . a = card (dom ({a} | p)) by A1; :: thesis: verum