let f be Function-yielding Function; :: thesis: rng (Frege f) c= product (rngs f)
let x be object ; :: 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 object such that
A1: y in dom (Frege f) and
A2: x = (Frege f) . y by FUNCT_1:def 3;
A3: dom (Frege f) = product (doms f) by Def6;
then consider g being Function such that
A4: y = g and
dom g = dom (doms f) and
A5: for z being object 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
A6: (Frege f) . g = h and
A7: dom h = dom f and
A8: for z being object st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) by A1, A3, A4, Def6;
A9: dom (rngs f) = dom f by Def2;
A10: dom (doms f) = dom f by Def1;

now :: thesis: for z being object st z in dom (rngs f) holds
h . z in (rngs f) . z

let z be object ; :: thesis: ( z in dom (rngs f) implies h . z in (rngs f) . z )
assume A11: z in dom (rngs f) ; :: thesis: h . z in (rngs f) . z
reconsider t = f . z as Function ;
A12: g . z in (doms f) . z by A5, A9, A10, A11;
A13: z in dom f by A9, A11;
then A14: (rngs f) . z = rng t by Th18;
A15: (doms f) . z = dom t by A13, Th18;
then A16: t . (g . z) in rng t by A12, FUNCT_1:def 3;
t . (g . z) = (uncurry f) . (z,(g . z)) by A13, A12, A15, FUNCT_5:38;
hence h . z in (rngs f) . z by A7, A8, A9, A11, A14, A16; :: thesis: verum

end;

hence x in product (rngs f) by A2, A4, A6, A7, A9, CARD_3:def 5; :: thesis: verum