theorem Th3: :: TOPGEN_5:3

for x, a being set
for f being Function st a in dom f holds
(commute (x .--> f)) . a = x .--> (f . a)