let X, Y be set ; :: thesis: for f being Function st rng f c= Funcs X,Y holds
( rng (uncurry f) c= Y & rng (uncurry' f) c= Y )
let f be Function; :: thesis: ( rng f c= Funcs X,Y implies ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) )
assume A1: rng f c= Funcs X,Y ; :: thesis: ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y )
Funcs X,Y c= PFuncs X,Y by FUNCT_2:141;
then rng f c= PFuncs X,Y by A1, XBOOLE_1:1;
hence ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) by Th47; :: thesis: verum