The project will be connected to proof mining as developed by Kohlenbach et al. since the 1990s. Proof mining concerns the analysis of given mathematical proofs using proof-theoretic tools and insights, with the aim of obtaining new information such as ef fective bounds or rates of convergence. The main areas of application have been nonlinear functional analysis, approximation theory, and ergodic theory, and recent metatheorems by Kohlenbach/Gerhardy concerning formal systems for analysis with various abs tract spaces as new ground types make possible the extraction of effective bounds from ineffective proofs of for-all-exist-statements s.t. the bounds are uniform in all parameters except through certain local bounds. These results can be used e.g. to obta in effective rates of metastability (in the sense of Tao) for iteration sequences, but not easily full rates of convergence - which is in general impossible. This reflects the fundamental difference between for-all-exist-for-all-statements and for-all-exi st-statements when it comes to obtaining effective bounds, and this situation obtains in many areas of mathematics. We have earlier nonetheless constructed explicit full rates of convergence for Picard iteration sequences of selfmaps of metric spaces in t wo case studies where there is convergence to a unique fixed point, and we gave an explanation for this (restricted to the bounded case) in the form of general conditions under which we in this setting can transform a for-all-exist-for-all-statement into a for-all-exist-statement via an argument involving product spaces. We aim mainly to clarify to what extent this approach can be lifted out of the particular setting of Picard iteration sequences in bounded metric spaces converging to a unique fixed point . Establishing nontrivial conditions under which a for-all-exist-for-all-statement behaves like a for-all-exist-statement is highly desirable in many areas of mathematics with respect to extracting effective bounds.