let x be object ; :: thesis: for f, g being Function st x in dom f & g = f . x holds
( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) )
let f, g be Function; :: thesis: ( x in dom f & g = f . x implies ( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) ) )
assume A1: ( x in dom f & g = f . x ) ; :: thesis: ( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) )
thus rng g c= rng (uncurry f) :: thesis: rng g c= rng (uncurry' f)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in rng (uncurry f) )
assume y in rng g ; :: thesis: y in rng (uncurry f)
then ex z being object st
( z in dom g & y = g . z ) by FUNCT_1:def 3;
hence y in rng (uncurry f) by A1, FUNCT_5:38; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in rng (uncurry' f) )
assume y in rng g ; :: thesis: y in rng (uncurry' f)
then ex z being object st
( z in dom g & y = g . z ) by FUNCT_1:def 3;
hence y in rng (uncurry' f) by A1, FUNCT_5:39; :: thesis: verum