@famesyasd Basically, let S = { g : n in nat and g in func({0..n},A) and g(0) = c and forall k in {1..n} ( g(k) = F(g(k−1)) ) }. Then prove that any two members f,g of S agree, namely if f in func({0..m},A) and g in func({0..n},A) such that m ≤ n, then forall k in {0..m} ( f(k) = g(k) ). Then you can 'glue' all the members of S to get the desired function. In ZFC, you would do this by constructing their union, since each function is just a set of pairs.