let x, y be object ; :: 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) ) )
assume that
A1: x in dom f and
A2: g = f . x and
A3: y in dom g ; :: thesis: ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y & g . y in rng (uncurry f) )
thus A4: [x,y] in dom (uncurry f) by A1, A2, A3, Def2; :: thesis: ( (uncurry f) . (x,y) = g . y & g . y in rng (uncurry f) )
( [x,y] `1 = x & [x,y] `2 = y ) ;
hence (uncurry f) . (x,y) = g . y by A2, A4, Def2; :: thesis: g . y in rng (uncurry f)
hence g . y in rng (uncurry f) by A4, FUNCT_1:def 3; :: thesis: verum