let X, Y be set ; :: thesis: for f being Function st rng f c= PFuncs (X,Y) holds
( rng (uncurry f) c= Y & rng (uncurry' f) c= Y )
let f be Function; :: thesis: ( rng f c= PFuncs (X,Y) implies ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) )
assume A1: rng f c= PFuncs (X,Y) ; :: thesis: ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y )
thus A2: rng (uncurry f) c= Y :: thesis: rng (uncurry' f) c= Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (uncurry f) or x in Y )
assume x in rng (uncurry f) ; :: thesis: x in Y
then consider y being object such that
A3: y in dom (uncurry f) and
A4: x = (uncurry f) . y by FUNCT_1:def 3;
consider z being object , g being Function, t being object such that
A5: y = [z,t] and
A6: ( z in dom f & g = f . z ) and
A7: t in dom g by A3, Def2;
g in rng f by A6, FUNCT_1:def 3;
then A8: ex g1 being Function st
( g = g1 & dom g1 c= X & rng g1 c= Y ) by A1, PARTFUN1:def 3;
( (uncurry f) . (z,t) = g . t & g . t in rng g ) by A6, A7, Th31, FUNCT_1:def 3;
hence x in Y by A4, A5, A8; :: thesis: verum

end;

rng (uncurry' f) c= rng (uncurry f) by FUNCT_4:41;
hence rng (uncurry' f) c= Y by A2; :: thesis: verum