Let FUF postulate the existence of a Free UltraFilter on $\mathbb{N}$ and ACC the axiom of countable choice. Is Consider the superstructure on $\mathbb{R}$ and its inclusion in the bounded ultrapower. Is there a reliable source proving that the transfer principle for this extension is provable in ZF+FUF+ACC?