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;

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 )
;

end;

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;( [x,y] `1 = x & [x,y] `2 = y ) ;

hence g . y = f .. (x,y) by A1, A2, A3, FUNCT_5:def 2; :: thesis: verum

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;

hence g . y = f .. (x,y) ; :: thesis: verum

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

then
( f .. (x,y) = 0 & g . y = 0 )
by A1, A2, A5, FUNCT_1:def 2;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 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

hence g . y = f .. (x,y) ; :: thesis: verum