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<sub>4</sub>(a) from FUNCT_2:sch 4();
m is Multiset of A by Th27;
hence ex b<sub>1</sub> being Multiset of A st
for a being Element of A holds b<sub>1</sub> . a = card (dom ({a} |` p)) by A1; :: thesis: verum