theorem Th6: :: TOPGEN_5:6

for a, b being set
for f, g being Function st a in dom f & g = f . a & b in dom g holds
((commute f) . b) . a = g . b