theorem Th23: :: PRALG_3:23

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
for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i