let X be set ; :: thesis: for f being Function holds
( dom (uncurry (X --> f)) = [:X,(dom f):] & rng (uncurry (X --> f)) c= rng f & dom (uncurry' (X --> f)) = [:(dom f),X:] & rng (uncurry' (X --> f)) c= rng f )
let f be Function; :: thesis: ( dom (uncurry (X --> f)) = [:X,(dom f):] & rng (uncurry (X --> f)) c= rng f & dom (uncurry' (X --> f)) = [:(dom f),X:] & rng (uncurry' (X --> f)) c= rng f )
f in Funcs ((dom f),(rng f)) by FUNCT_2:def 2;
then ( rng (X --> f) c= {f} & {f} c= Funcs ((dom f),(rng f)) ) by FUNCOP_1:13, ZFMISC_1:31;
then ( dom (X --> f) = X & rng (X --> f) c= Funcs ((dom f),(rng f)) ) ;
hence ( dom (uncurry (X --> f)) = [:X,(dom f):] & rng (uncurry (X --> f)) c= rng f & dom (uncurry' (X --> f)) = [:(dom f),X:] & rng (uncurry' (X --> f)) c= rng f ) by FUNCT_5:26, FUNCT_5:41; :: thesis: verum