let X be set ; :: thesis: for f being Function st X <> {} holds
( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f )
let f be Function; :: thesis: ( X <> {} implies ( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f ) )
set x = the Element of X;
assume A1: X <> {} ; :: thesis: ( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f )
then ( dom (X --> f) = X & (X --> f) . the Element of X = f ) by FUNCOP_1:7;
hence ( rng (uncurry (X --> f)) c= rng f & rng f c= rng (uncurry (X --> f)) & rng (uncurry' (X --> f)) c= rng f & rng f c= rng (uncurry' (X --> f)) ) by A1, Th7, Th8; :: according to XBOOLE_0:def 10 :: thesis: verum