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 )
A1: ( dom (X --> f) = X & rng (X --> f) c= {f} & f in Funcs (dom f),(rng f) ) by FUNCOP_1:19, FUNCT_2:def 2;
then {f} c= Funcs (dom f),(rng f) by ZFMISC_1:37;
then rng (X --> f) c= Funcs (dom f),(rng f) by A1, XBOOLE_1:1;
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 A1, FUNCT_5:33, FUNCT_5:48; :: thesis: verum