theorem Th20: :: TIETZE_2:1

for X, Y being set
for F being Function-yielding Function
for x, y being object st ( F is Funcs (X,Y) -valued or y in dom <:F:> ) holds
(F . x) . y = (<:F:> . y) . x