let x, y be object ; :: 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 A1: ( 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 [x,y] in dom (uncurry f) by Th31;
hence A2: [y,x] in dom (uncurry' f) by FUNCT_4:42; :: thesis: ( (uncurry' f) . (y,x) = g . y & g . y in rng (uncurry' f) )
(uncurry f) . (x,y) = g . y by A1, Th31;
hence (uncurry' f) . (y,x) = g . y by A2, FUNCT_4:43; :: thesis: g . y in rng (uncurry' f)
hence g . y in rng (uncurry' f) by A2, FUNCT_1:def 3; :: thesis: verum