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 ) )
assume A1: X <> {} ; :: thesis: ( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f )
consider x being Element of X;
( dom (X --> f) = X & (X --> f) . x = f ) by A1, FUNCOP_1:13, FUNCOP_1:19;
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, Th16, Th17; :: according to XBOOLE_0:def 10 :: thesis: verum