theorem :: FUNCT_6:35

for x, y being object
for f being Function-yielding Function st x in dom f & f . x is Function & y in dom <:f:> holds
f .. (x,y) = <:f:> .. (y,x)