theorem Th7: :: PRALG_3:7

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))