let x, y be set ; :: thesis: for f, g being Function st g = f . x holds
g . y = f .. (x,y)
let f, g be Function; :: thesis: ( g = f . x implies g . y = f .. (x,y) )
assume A1: g = f . x ; :: thesis: g . y = f .. (x,y)
A2: f .. (x,y) = (uncurry f) . (x,y) by FUNCT_6:def 5;

per cases ( ( x in dom f & y in dom g ) or y nin dom g or x nin dom f ) ;

suppose ( x in dom f & y in dom g ) ; :: thesis: g . y = f .. (x,y)

then A3: ( [x,y] in dom (uncurry f) & f . ([x,y] `1) is Function ) by A1, FUNCT_5:def 2;
( [x,y] `1 = x & [x,y] `2 = y ) ;
hence g . y = f .. (x,y) by A1, A2, A3, FUNCT_5:def 2; :: thesis: verum

end;

suppose A4: ( y nin dom g or x nin dom f ) ; :: thesis: g . y = f .. (x,y)

then A5: ( ( f . x = 0 or g . y = 0 ) & dom {} = {} ) by FUNCT_1:def 2;

now :: thesis: not [x,y] in dom (uncurry f)

assume [x,y] in dom (uncurry f) ; :: thesis: contradiction
then consider a being object , h being Function, b being object such that
A6: ( [x,y] = [a,b] & a in dom f & h = f . a & b in dom h ) by FUNCT_5:def 2;
( a = x & b = y ) by A6, XTUPLE_0:1;
hence contradiction by A1, A4, A6; :: thesis: verum

end;

then ( f .. (x,y) = 0 & g . y = 0 ) by A1, A2, A5, FUNCT_1:def 2;
hence g . y = f .. (x,y) ; :: thesis: verum

end;

end;