theorem Th20: :: PRALG_3:20

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))