let x, y be object ; 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; ( 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 )
; ( [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; ( (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; g . y in rng (uncurry' f)
hence
g . y in rng (uncurry' f)
by A2, FUNCT_1:def 3; verum