let f be Function; :: thesis: rng (Frege f) c= product (rngs f)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Frege f) or x in product (rngs f) )
assume x in rng (Frege f) ; :: thesis: x in product (rngs f)
then consider y being set such that
A1: ( y in dom (Frege f) & x = (Frege f) . y ) by FUNCT_1:def 5;
A2: dom (Frege f) = product (doms f) by Def7;
then consider g being Function such that
A3: ( y = g & dom g = dom (doms f) & ( for z being set st z in dom (doms f) holds
g . z in (doms f) . z ) ) by A1, CARD_3:def 5;
consider h being Function such that
A4: ( (Frege f) . g = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds
h . z = (uncurry f) . z,(g . z) ) ) by A1, A2, A3, Def7;
A5: ( dom (rngs f) = f " (SubFuncs (rng f)) & dom (doms f) = f " (SubFuncs (rng f)) ) by Def2, Def3;

now

let z be set ; :: thesis: ( z in dom (rngs f) implies h . z in (rngs f) . z )
assume A6: z in dom (rngs f) ; :: thesis: h . z in (rngs f) . z
then A7: ( z in dom f & f . z in SubFuncs (rng f) & z in dom h & g . z in (doms f) . z ) by A3, A4, A5, FUNCT_1:def 13;
then reconsider t = f . z as Function by Def1;
A8: ( (rngs f) . z = rng t & (doms f) . z = dom t ) by A7, Th31;
then ( t . (g . z) in rng t & t . (g . z) = (uncurry f) . z,(g . z) ) by A7, FUNCT_1:def 5, FUNCT_5:45;
hence h . z in (rngs f) . z by A4, A5, A6, A8; :: thesis: verum

end;

hence x in product (rngs f) by A1, A3, A4, A5, CARD_3:def 5; :: thesis: verum