let x be object ; for f, g being Function st x in dom (curry f) & g = (curry f) . x holds
( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f ) ) )
let f, g be Function; ( x in dom (curry f) & g = (curry f) . x implies ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f ) ) ) )
assume that
A1:
x in dom (curry f)
and
A2:
g = (curry f) . x
; ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f ) ) )
dom (curry f) = proj1 (dom f)
by Def1;
then consider h being Function such that
A3:
(curry f) . x = h
and
A4:
dom h = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):])
and
A5:
for y being object st y in dom h holds
h . y = f . (x,y)
by A1, Def1;
thus
dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):])
by A2, A3, A4; ( dom g c= proj2 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f ) ) )
(dom f) /\ [:{x},(proj2 (dom f)):] c= dom f
by XBOOLE_1:17;
hence
dom g c= proj2 (dom f)
by A2, A3, A4, XTUPLE_0:9; ( rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f ) ) )
thus
rng g c= rng f
for y being object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f )proof
let y be
object ;
TARSKI:def 3 ( not y in rng g or y in rng f )
assume
y in rng g
;
y in rng f
then consider z being
object such that A6:
z in dom g
and A7:
y = g . z
by FUNCT_1:def 3;
consider t being
object such that A8:
[t,z] in (dom f) /\ [:{x},(proj2 (dom f)):]
by A2, A3, A4, A6, XTUPLE_0:def 13;
(
[t,z] in dom f &
[t,z] in [:{x},(proj2 (dom f)):] )
by A8, XBOOLE_0:def 4;
then A9:
[x,z] in dom f
by ZFMISC_1:105;
h . z = f . (
x,
z)
by A2, A3, A5, A6;
hence
y in rng f
by A2, A3, A7, A9, FUNCT_1:def 3;
verum
end;
let y be object ; ( y in dom g implies ( g . y = f . (x,y) & [x,y] in dom f ) )
assume A10:
y in dom g
; ( g . y = f . (x,y) & [x,y] in dom f )
then consider t being object such that
A11:
[t,y] in (dom f) /\ [:{x},(proj2 (dom f)):]
by A2, A3, A4, XTUPLE_0:def 13;
( [t,y] in dom f & [t,y] in [:{x},(proj2 (dom f)):] )
by A11, XBOOLE_0:def 4;
hence
( g . y = f . (x,y) & [x,y] in dom f )
by A2, A3, A5, A10, ZFMISC_1:105; verum