let X, Y be set ; for f being Function st rng f c= PFuncs (X,Y) holds
( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] )
let f be Function; ( rng f c= PFuncs (X,Y) implies ( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] ) )
assume A1:
rng f c= PFuncs (X,Y)
; ( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] )
thus A2:
dom (uncurry f) c= [:(dom f),X:]
dom (uncurry' f) c= [:X,(dom f):]proof
let x be
object ;
TARSKI:def 3 ( not x in dom (uncurry f) or x in [:(dom f),X:] )
assume
x in dom (uncurry f)
;
x in [:(dom f),X:]
then consider y being
object ,
g being
Function,
z being
object such that A3:
x = [y,z]
and A4:
y in dom f
and A5:
g = f . y
and A6:
z in dom g
by Def2;
g in rng f
by A4, A5, FUNCT_1:def 3;
then
g is
PartFunc of
X,
Y
by A1, PARTFUN1:46;
then
dom g c= X
by RELAT_1:def 18;
hence
x in [:(dom f),X:]
by A3, A4, A6, ZFMISC_1:87;
verum
end;
let x be object ; TARSKI:def 3 ( not x in dom (uncurry' f) or x in [:X,(dom f):] )
assume
x in dom (uncurry' f)
; x in [:X,(dom f):]
then
ex y, z being object st
( x = [z,y] & [y,z] in dom (uncurry f) )
by FUNCT_4:def 2;
hence
x in [:X,(dom f):]
by A2, ZFMISC_1:88; verum