let x, y be set ; :: thesis: for f, g being Function st x in dom f & g = f . x & y in dom g holds
( [y,x] in dom (uncurry' f) & (uncurry' f) . y,x = g . y & g . y in rng (uncurry' f) )
let f, g be Function; :: thesis: ( x in dom f & g = f . x & y in dom g implies ( [y,x] in dom (uncurry' f) & (uncurry' f) . y,x = g . y & g . y in rng (uncurry' f) ) )
assume ( x in dom f & g = f . x & y in dom g ) ; :: thesis: ( [y,x] in dom (uncurry' f) & (uncurry' f) . y,x = g . y & g . y in rng (uncurry' f) )
then A1: ( [x,y] in dom (uncurry f) & (uncurry f) . x,y = g . y & g . y in rng (uncurry f) & uncurry' f = ~ (uncurry f) ) by Th45;
hence A2: [y,x] in dom (uncurry' f) by FUNCT_4:43; :: thesis: ( (uncurry' f) . y,x = g . y & g . y in rng (uncurry' f) )
hence (uncurry' f) . y,x = g . y by A1, FUNCT_4:44; :: thesis: g . y in rng (uncurry' f)
hence g . y in rng (uncurry' f) by A2, FUNCT_1:def 5; :: thesis: verum