let x, y be set ; :: thesis: for f, g being Function st x in dom f & g = f . x & y in dom g holds
( [x,y] in dom (uncurry f) & (uncurry f) . x,y = 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 ( [x,y] in dom (uncurry f) & (uncurry f) . x,y = g . y & g . y in rng (uncurry f) ) )
A1: ( [x,y] `1 = x & [x,y] `2 = y ) by MCART_1:7;
assume A2: ( x in dom f & g = f . x & y in dom g ) ; :: thesis: ( [x,y] in dom (uncurry f) & (uncurry f) . x,y = g . y & g . y in rng (uncurry f) )
hence A3: [x,y] in dom (uncurry f) by Def4; :: thesis: ( (uncurry f) . x,y = g . y & g . y in rng (uncurry f) )
hence (uncurry f) . x,y = g . y by A1, A2, Def4; :: thesis: g . y in rng (uncurry f)
hence g . y in rng (uncurry f) by A3, FUNCT_1:def 5; :: thesis: verum