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 object ; :: 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 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; :: thesis: verum

end;

let x be object ; :: 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 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; :: thesis: verum