let f be Function-yielding Function; :: thesis: product (rngs f) c= rng (Frege f)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product (rngs f) or x in rng (Frege f) )
deffunc H₁( object ) -> set = (doms f) . $1;
assume x in product (rngs f) ; :: thesis: x in rng (Frege f)
then consider g being Function such that
A1: x = g and
A2: dom g = dom (rngs f) and
A3: for y being object st y in dom (rngs f) holds
g . y in (rngs f) . y by CARD_3:def 5;
defpred S₁[ object , object ] means ex f1 being Function st
( f1 = f . $1 & f1 . $2 = g . $1 );
consider h being Function such that
A4: ( dom h = dom f & ( for x being object st x in dom f holds
for y being object holds
( y in h . x iff ( y in H₁(x) & S₁[x,y] ) ) ) ) from CARD_3:sch 2();
A5: product (doms f) = dom (Frege f) by Def6;
A6: dom (doms f) = dom f by Def1;
A7: dom (rngs f) = dom f by Def2;

A8: now :: thesis: for X being set st X in rng h holds
X <> {}

let X be set ; :: thesis: ( X in rng h implies X <> {} )
assume X in rng h ; :: thesis: X <> {}
then consider x being object such that
A9: x in dom h and
A10: X = h . x by FUNCT_1:def 3;
reconsider fx = f . x as Function ;
A11: x in dom f by A4, A9;
then A12: (rngs f) . x = rng fx by Th18;
g . x in (rngs f) . x by A3, A7, A4, A9;
then A13: ex y being object st
( y in dom fx & g . x = fx . y ) by A12, FUNCT_1:def 3;
(doms f) . x = dom fx by A11, Th18;
hence X <> {} by A4, A9, A10, A13; :: thesis: verum

end;

A14: now :: thesis: ( dom f <> {} implies x in rng (Frege f) )

assume dom f <> {} ; :: thesis: x in rng (Frege f)
then reconsider D = rng h as non empty set by A4, RELAT_1:42;
consider Ch being Function such that
A15: dom Ch = D and
A16: for x being set st x in D holds
Ch . x in x by A8, FUNCT_1:111;
A17: dom (Ch * h) = dom h by A15, RELAT_1:27;

now :: thesis: for y being object st y in dom (doms f) holds
(Ch * h) . y in (doms f) . y

let y be object ; :: thesis: ( y in dom (doms f) implies (Ch * h) . y in (doms f) . y )
assume A18: y in dom (doms f) ; :: thesis: (Ch * h) . y in (doms f) . y
then ( (Ch * h) . y = Ch . (h . y) & h . y in rng h ) by A6, A4, A17, FUNCT_1:12, FUNCT_1:def 3;
then (Ch * h) . y in h . y by A16;
hence (Ch * h) . y in (doms f) . y by A6, A4, A18; :: thesis: verum

end;

then A19: Ch * h in product (doms f) by A6, A4, A17, CARD_3:def 5;
then consider h1 being Function such that
A20: (Frege f) . (Ch * h) = h1 and
A21: dom h1 = dom f and
A22: for x being object st x in dom h1 holds
h1 . x = (uncurry f) . (x,((Ch * h) . x)) by Def6;

now :: thesis: for z being object st z in dom f holds
h1 . z = g . z

let z be object ; :: thesis: ( z in dom f implies h1 . z = g . z )
assume A23: z in dom f ; :: thesis: h1 . z = g . z
then A24: h1 . z = (uncurry f) . (z,((Ch * h) . z)) by A21, A22;
( (Ch * h) . z = Ch . (h . z) & h . z in rng h ) by A4, A17, A23, FUNCT_1:12, FUNCT_1:def 3;
then A25: (Ch * h) . z in h . z by A16;
then consider f1 being Function such that
A26: f1 = f . z and
A27: f1 . ((Ch * h) . z) = g . z by A4, A23;
A28: (Ch * h) . z in (doms f) . z by A4, A23, A25;
A29: z in dom f by A23;
then (doms f) . z = dom f1 by A26, Th18;
hence h1 . z = g . z by A29, A24, A26, A27, A28, FUNCT_5:38; :: thesis: verum

end;

then x = h1 by A1, A2, A7, A21, FUNCT_1:2;
hence x in rng (Frege f) by A5, A19, A20, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: ( dom f = {} implies x in rng (Frege f) )

assume A30: dom f = {} ; :: thesis: x in rng (Frege f)
then A31: g = {} by A2, Def2;
dom (Frege f) = {{}} by A6, A5, A30, CARD_3:10, RELAT_1:41;
then A32: {} in dom (Frege f) by TARSKI:def 1;
then consider h being Function such that
A33: (Frege f) . {} = h and
A34: dom h = dom f and
for x being object st x in dom h holds
h . x = (uncurry f) . (x,({} . x)) by A5, Def6;
h = {} by A30, A34;
hence x in rng (Frege f) by A1, A31, A32, A33, FUNCT_1:def 3; :: thesis: verum

end;

hence x in rng (Frege f) by A14; :: thesis: verum