let X, Y be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] )
thus A2: dom (uncurry f) c= [:(dom f),X:] :: thesis: dom (uncurry' f) c= [:X,(dom f):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (uncurry f) or x in [:(dom f),X:] )
assume x in dom (uncurry f) ; :: thesis: x in [:(dom f),X:]
then consider y being set , g being Function, z being set such that
A3: ( x = [y,z] & y in dom f & g = f . y & z in dom g ) by Def4;
g in rng f by A3, FUNCT_1:def 5;
then g is PartFunc of X,Y by A1, PARTFUN1:120;
then dom g c= X by RELAT_1:def 18;
hence x in [:(dom f),X:] by A3, ZFMISC_1:106; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (uncurry' f) or x in [:X,(dom f):] )
assume x in dom (uncurry' f) ; :: thesis: x in [:X,(dom f):]
then consider y, z being set such that
A4: ( x = [z,y] & [y,z] in dom (uncurry f) ) by FUNCT_4:def 2;
thus x in [:X,(dom f):] by A2, A4, ZFMISC_1:107; :: thesis: verum