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 ) )
A1: Funcs (X,Y) c= PFuncs (X,Y) by FUNCT_2:72;
assume rng f c= Funcs (X,Y) ; :: thesis: ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y )
then rng f c= PFuncs (X,Y) by A1;
hence ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) by Th33; :: thesis: verum