let f be Function; rng (Frege f) c= product (rngs f)
let x be set ; TARSKI:def 3 ( not x in rng (Frege f) or x in product (rngs f) )
assume
x in rng (Frege f)
; x in product (rngs f)
then consider y being set 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 Def7;
then consider g being Function such that
A4:
y = g
and
dom g = dom (doms f)
and
A5:
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
A6:
(Frege f) . g = h
and
A7:
dom h = f " (SubFuncs (rng f))
and
A8:
for z being set st z in dom h holds
h . z = (uncurry f) . (z,(g . z))
by A1, A3, A4, Def7;
A9:
dom (rngs f) = f " (SubFuncs (rng f))
by Def3;
A10:
dom (doms f) = f " (SubFuncs (rng f))
by Def2;
now let z be
set ;
( z in dom (rngs f) implies h . z in (rngs f) . z )assume A11:
z in dom (rngs f)
;
h . z in (rngs f) . zthen
f . z in SubFuncs (rng f)
by A9, FUNCT_1:def 7;
then reconsider t =
f . z as
Function by Def1;
A12:
g . z in (doms f) . z
by A5, A9, A10, A11;
A13:
z in dom f
by A9, A11, FUNCT_1:def 7;
then A14:
(rngs f) . z = rng t
by Th31;
A15:
(doms f) . z = dom t
by A13, Th31;
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;
verum end;
hence
x in product (rngs f)
by A2, A4, A6, A7, A9, CARD_3:def 5; verum