theorem Th7: :: TOPGEN_5:7

for a being set
for f, g, h being Function st h = f \/ g holds
(commute h) . a = ((commute f) . a) \/ ((commute g) . a)