let f be Function; ( rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f)) & rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) )
A1:
rng (~ f) c= rng f
by FUNCT_4:41;
thus
rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f))
rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f))proof
let t be
object ;
TARSKI:def 3 ( not t in rng (curry f) or t in PFuncs ((proj2 (dom f)),(rng f)) )
assume
t in rng (curry f)
;
t in PFuncs ((proj2 (dom f)),(rng f))
then consider z being
object such that A2:
z in dom (curry f)
and A3:
t = (curry f) . z
by FUNCT_1:def 3;
dom (curry f) = proj1 (dom f)
by Def1;
then consider g being
Function such that A4:
(curry f) . z = g
and
dom g = proj2 ((dom f) /\ [:{z},(proj2 (dom f)):])
and
for
y being
object st
y in dom g holds
g . y = f . (
z,
y)
by A2, Def1;
(
dom g c= proj2 (dom f) &
rng g c= rng f )
by A2, A4, Th24;
hence
t in PFuncs (
(proj2 (dom f)),
(rng f))
by A3, A4, PARTFUN1:def 3;
verum
end;
let t be object ; TARSKI:def 3 ( not t in rng (curry' f) or t in PFuncs ((proj1 (dom f)),(rng f)) )
assume
t in rng (curry' f)
; t in PFuncs ((proj1 (dom f)),(rng f))
then consider z being object such that
A5:
z in dom (curry' f)
and
A6:
t = (curry' f) . z
by FUNCT_1:def 3;
dom (curry (~ f)) = proj1 (dom (~ f))
by Def1;
then consider g being Function such that
A7:
(curry (~ f)) . z = g
and
dom g = proj2 ((dom (~ f)) /\ [:{z},(proj2 (dom (~ f))):])
and
for y being object st y in dom g holds
g . y = (~ f) . (z,y)
by A5, Def1;
rng g c= rng (~ f)
by A5, A7, Th24;
then A8:
rng g c= rng f
by A1;
dom g c= proj2 (dom (~ f))
by A5, A7, Th24;
then
dom g c= proj1 (dom f)
by Th11;
hence
t in PFuncs ((proj1 (dom f)),(rng f))
by A6, A7, A8, PARTFUN1:def 3; verum