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

A4: now

let X be set ; :: thesis: ( X in rng h implies X <> {} )
assume X in rng h ; :: thesis: X <> {}
then consider x being set such that
A5: ( x in dom h & X = h . x ) by FUNCT_1:def 5;
A6: ( x in dom f & f . x in SubFuncs (rng f) ) by A3, A5, FUNCT_1:def 13;
then reconsider fx = f . x as Function by Def1;
( (rngs f) . x = rng fx & g . x in (rngs f) . x ) by A1, A2, A3, A5, A6, Th31;
then consider y being set such that
A7: ( y in dom fx & g . x = fx . y ) by FUNCT_1:def 5;
(doms f) . x = dom fx by A6, Th31;
hence X <> {} by A3, A5, A7; :: thesis: verum

end;

A8: now

assume A9: f " (SubFuncs (rng f)) = {} ; :: thesis: x in rng (Frege f)
then A10: ( g = {} & doms f = {} ) by A1, A2;
dom (Frege f) = {{} } by A2, A9, CARD_3:19, RELAT_1:64;
then A11: {} in dom (Frege f) by TARSKI:def 1;
then consider h being Function such that
A12: ( (Frege f) . {} = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . x,({} . x) ) ) by A2, Def7;
h = {} by A9, A12;
hence x in rng (Frege f) by A1, A10, A11, A12, FUNCT_1:def 5; :: thesis: verum

end;

now

assume f " (SubFuncs (rng f)) <> {} ; :: thesis: x in rng (Frege f)
then reconsider D = rng h as non empty set by A3, RELAT_1:65;
consider Ch being Function such that
A13: ( dom Ch = D & ( for x being set st x in D holds
Ch . x in x ) ) by A4, WELLORD2:28;
A14: dom (Ch * h) = dom h by A13, RELAT_1:46;

now

let y be set ; :: thesis: ( y in dom (doms f) implies (Ch * h) . y in (doms f) . y )
assume A15: 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 A2, A3, A14, FUNCT_1:22, FUNCT_1:def 5;
then (Ch * h) . y in h . y by A13;
hence (Ch * h) . y in (doms f) . y by A2, A3, A15; :: thesis: verum

end;

then A16: Ch * h in product (doms f) by A2, A3, A14, CARD_3:def 5;
then consider h1 being Function such that
A17: ( (Frege f) . (Ch * h) = h1 & dom h1 = f " (SubFuncs (rng f)) & ( for x being set st x in dom h1 holds
h1 . x = (uncurry f) . x,((Ch * h) . x) ) ) by Def7;

now

let z be set ; :: thesis: ( z in f " (SubFuncs (rng f)) implies h1 . z = g . z )
assume A18: z in f " (SubFuncs (rng f)) ; :: thesis: h1 . z = g . z
then A19: ( z in dom f & h1 . z = (uncurry f) . z,((Ch * h) . z) & (Ch * h) . z = Ch . (h . z) & h . z in rng h ) by A3, A14, A17, FUNCT_1:22, FUNCT_1:def 5, FUNCT_1:def 13;
then A20: (Ch * h) . z in h . z by A13;
then consider f1 being Function such that
A21: ( f1 = f . z & f1 . ((Ch * h) . z) = g . z ) by A3, A18;
( (Ch * h) . z in (doms f) . z & (doms f) . z = dom f1 ) by A3, A18, A19, A20, A21, Th31;
hence h1 . z = g . z by A19, A21, FUNCT_5:45; :: thesis: verum

end;

then x = h1 by A1, A2, A17, FUNCT_1:9;
hence x in rng (Frege f) by A2, A16, A17, FUNCT_1:def 5; :: thesis: verum

end;

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