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 that
A1: ( x in dom f & g = f . x ) and
A2: y in dom <:f:> and
A3: h = <:f:> . y ; :: thesis: g . y = h . x
dom h = f " (SubFuncs (rng f)) by A2, A3, Th51;
then x in dom h by A1, Th28;
then A4: h . x = (uncurry f) . (x,y) by A2, A3, Th51;
g in rng f by A1, FUNCT_1:def 5;
then y in dom g by A2, Th52;
hence g . y = h . x by A1, A4, FUNCT_5:45; :: thesis: verum