for f being Function-yielding Function holds rng (Frege f) = product (rngs f) by Lm1, Lm2;