let x, y be object ; :: thesis: for g, h being Function
for f being Function-yielding Function st x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y holds
g . y = h . x
let g, h be Function; :: thesis: for f being Function-yielding Function st x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y holds
g . y = h . x
let f be Function-yielding 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 = dom f by A2, A3, Th26;
then x in dom h by A1;
then A4: h . x = (uncurry f) . (x,y) by A2, A3, Th26;
g in rng f by A1, FUNCT_1:def 3;
then y in dom g by A2, Th27;
hence g . y = h . x by A1, A4, FUNCT_5:38; :: thesis: verum