theorem Th106: :: FUNCT_7:107

for x, y, a being object
for f being Function st f . x = f . y holds
f . a = (f * ((id (dom f)) +* (x,y))) . a