:: deftheorem Def5 defines commute WAYBEL29:def 5 :
for M being non empty set
for X, Y being non empty TopSpace
for b₄ being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) holds
( b₄ = commute (X,M,Y) iff for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b₄ . f = commute f );