let x, y be set ; :: thesis: for f, g, h being Function st x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y holds
g . y = h . x
let f, g, h be Function; :: thesis: ( x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y implies g . y = h . x )
assume A1: ( x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y ) ; :: thesis: g . y = h . x
then dom h = f " (SubFuncs (rng f)) by Th51;
then ( x in dom h & g in rng f ) by A1, Th28, FUNCT_1:def 5;
then ( h . x = (uncurry f) . x,y & y in dom g ) by A1, Th51, Th52;
hence g . y = h . x by A1, FUNCT_5:45; :: thesis: verum