let f be Function; :: thesis: rng (Frege f) = product (rngs f)
thus ( rng (Frege f) c= product (rngs f) & product (rngs f) c= rng (Frege f) ) by Lm2, Lm3; :: according to XBOOLE_0:def 10 :: thesis: verum